Theorem brrelexi 3198

Description: The first argument of a binary relation exists. (An artifact of our ordered pair definition.)

Hypothesis

Ref	Expression
brrelexi.1	|- Rel R

Assertion

Ref	Expression
brrelexi	|- (ARB -> A e. V)

Proof of Theorem brrelexi

Step	Hyp	Ref	Expression
1		brrelexi.1	. 2 |- Rel R
2		brrelex 3197	. 2 |- ((Rel R /\ ARB) -> A e. V)
3	1, 2	mpan 693	1 |- (ARB -> A e. V)

Syntax hints:   -> wi 3   e. wcel 955  Vcvv 1802   class class class wbr 2609  Rel wrel 3165

This theorem is referenced by:  nprrel 3199  vtoclr 3201  vtoclrbr 3202  vtoclibr 3203  ideqg 3266  issetid 3269  oprprc1 3969  breng 4357  brdomg 4358  ensymg 4392  unen 4414  xpdom2 4422  xpdom1 4423  sbth 4437  domnsym 4443  ensdomtr 4451  sdomirr 4452  sdomex 4453  domsdomtr 4456  sdomen2 4462  fodomr 4463  pwen 4483  php3 4495  infsdomnn 4511  domfi 4516  unifi 4532  fodomfi 4540  fodomfib 4541  iunfi 4543  pwfi 4545  card1 4805  alephnbtwn2 4841  alephsucdom 4852  prcdpq 5069  climcl 6916  clmi1 7024  climaddc 7068  climmulc 7069  climabslem 7084  unctb 7519  eltopsp 7546  tpsex 7547  ismsg 7739  isring 8078  isvcgOLD 8133

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-br 2610  df-opab 2657  df-xp 3174  df-rel 3175

Copyright terms: Public domain