Theorem brrelex1i 5741

Description: The first argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by NM, 4-Jun-1998.)

Hypothesis

Ref	Expression
brrelexi.1	⊢ Rel 𝑅

Assertion

Ref	Expression
brrelex1i	⊢ (𝐴𝑅𝐵 → 𝐴 ∈ V)

Proof of Theorem brrelex1i

Step	Hyp	Ref	Expression
1		brrelexi.1	. 2 ⊢ Rel 𝑅
2		brrelex1 5738	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
3	1, 2	mpan 690	1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480   class class class wbr 5143  Rel wrel 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692

This theorem is referenced by:  nprrel  5744  opeliunxp2  5849  ideqg  5862  issetid  5865  dffv2  7004  brfvopabrbr  7013  brrpssg  7745  opeliunxp2f  8235  brtpos2  8257  brdomg  8997  brdomgOLD  8998  ctex  9004  isfi  9016  domssr  9039  domdifsn  9094  undomOLD  9100  xpdom2  9107  xpdom1g  9109  sucdom2OLD  9122  sbth  9133  dom0OLD  9143  sdom0OLD  9149  sdomirr  9154  sdomdif  9165  fodomr  9168  pwdom  9169  xpen  9180  pwen  9190  sbthfi  9239  sucdom2  9243  php3OLD  9261  sdom1OLD  9279  fineqv  9299  f1finf1oOLD  9306  infsdomnn  9338  infsdomnnOLD  9339  relprcnfsupp  9404  fsuppssov1  9424  fsuppunbi  9429  mapfien2  9449  harword  9603  brwdom  9607  domwdom  9614  brwdom3i  9623  unwdomg  9624  xpwdomg  9625  infdifsn  9697  ac10ct  10074  inffien  10103  djuen  10210  djudom2  10224  djufi  10227  cdainflem  10228  djulepw  10233  infdjuabs  10245  infunabs  10246  infmap2  10257  cfslb2n  10308  fin4i  10338  isfin5  10339  isfin6  10340  fin4en1  10349  isfin4p1  10355  isfin32i  10405  fin45  10432  fin56  10433  fin67  10435  hsmexlem1  10466  hsmexlem3  10468  axcc3  10478  ttukeylem1  10549  brdom3  10568  iundom2g  10580  iundom  10582  gchi  10664  engch  10668  gchdomtri  10669  fpwwe2lem5  10675  fpwwe2lem6  10676  fpwwe2lem8  10678  gchdjuidm  10708  gchpwdom  10710  prcdnq  11033  reexALT  13026  hasheni  14387  hashdomi  14419  climcl  15535  climi  15546  climrlim2  15583  climrecl  15619  climge0  15620  iseralt  15721  climfsum  15856  structex  17187  issubc  17880  pmtrfv  19470  dprdval  20023  frgpcyg  21592  lindff  21835  lindfind  21836  f1lindf  21842  lindfmm  21847  lsslindf  21850  lbslcic  21861  psrbaglesupp  21942  hauspwdom  23509  refbas  23518  refssex  23519  reftr  23522  refun0  23523  ovoliunnul  25542  dvle  26046  cyclnspth  29821  hlimi  31207  gsumhashmul  33064  extdgval  33705  usgrgt2cycl  35135  brsset  35890  brbigcup  35899  elfix2  35905  brcolinear2  36059  isfne  36340  refssfne  36359  bj-epelg  37069  bj-ideqb  37160  bj-opelidb1ALT  37167  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  brabg2  37724  heiborlem4  37821  isrngo  37904  isdivrngo  37957  brssr  38502  issetssr  38504  fphpd  42827  ctbnfien  42829  sdomne0  43426  climd  45687  climuzlem  45758  rlimdmafv  47189  rlimdmafv2  47270  fuco112  49024  fuco111  49025  fuco21  49031  fucoid  49043