Theorem brrelex1i 5654

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 5651	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
3	1, 2	mpan 688	1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2104  Vcvv 3437   class class class wbr 5081  Rel wrel 5605

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3063  df-rex 3072  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-br 5082  df-opab 5144  df-xp 5606  df-rel 5607

This theorem is referenced by:  nprrel  5657  opeliunxp2  5760  ideqg  5773  issetid  5776  dffv2  6895  brfvopabrbr  6904  brrpssg  7610  opeliunxp2f  8057  brtpos2  8079  brdomg  8777  brdomgOLD  8778  ctex  8784  isfi  8797  domssr  8820  en1unielOLD  8854  domdifsn  8879  undomOLD  8885  xpdom2  8892  xpdom1g  8894  sucdom2OLD  8907  sbth  8918  dom0OLD  8928  sdom0OLD  8934  sdomirr  8939  sdomdif  8950  fodomr  8953  pwdom  8954  xpen  8965  pwen  8975  sbthfi  9023  sucdom2  9027  php3OLD  9045  sdom1OLD  9064  fineqv  9082  f1finf1o  9090  infsdomnn  9119  relprcnfsupp  9175  fsuppunbi  9193  mapfien2  9212  harword  9366  brwdom  9370  domwdom  9377  brwdom3i  9386  unwdomg  9387  xpwdomg  9388  infdifsn  9459  ac10ct  9836  inffien  9865  djuen  9971  djudom2  9985  djufi  9988  cdainflem  9989  djulepw  9994  infdjuabs  10008  infunabs  10009  infmap2  10020  cfslb2n  10070  fin4i  10100  isfin5  10101  isfin6  10102  fin4en1  10111  isfin4p1  10117  isfin32i  10167  fin45  10194  fin56  10195  fin67  10197  hsmexlem1  10228  hsmexlem3  10230  axcc3  10240  ttukeylem1  10311  brdom3  10330  iundom2g  10342  iundom  10344  gchi  10426  engch  10430  gchdomtri  10431  fpwwe2lem5  10437  fpwwe2lem6  10438  fpwwe2lem8  10440  gchdjuidm  10470  gchpwdom  10472  prcdnq  10795  reexALT  12770  hasheni  14108  hashdomi  14140  climcl  15253  climi  15264  climrlim2  15301  climrecl  15337  climge0  15338  iseralt  15441  climfsum  15577  structex  16896  issubc  17595  pmtrfv  19105  dprdval  19651  frgpcyg  20826  lindff  21067  lindfind  21068  f1lindf  21074  lindfmm  21079  lsslindf  21082  lbslcic  21093  psrbaglesupp  21172  hauspwdom  22697  refbas  22706  refssex  22707  reftr  22710  refun0  22711  ovoliunnul  24716  dvle  25216  cyclnspth  28213  hlimi  29595  gsumhashmul  31361  extdgval  31774  usgrgt2cycl  33137  brsset  34236  brbigcup  34245  elfix2  34251  brcolinear2  34405  isfne  34573  refssfne  34592  bj-epelg  35283  bj-ideqb  35374  bj-opelidb1ALT  35381  ovoliunnfl  35863  voliunnfl  35865  volsupnfl  35866  brabg2  35918  heiborlem4  36016  isrngo  36099  isdivrngo  36152  brssr  36661  issetssr  36663  fphpd  40675  ctbnfien  40677  climd  43262  climuzlem  43333  rlimdmafv  44727  rlimdmafv2  44808