Theorem brrelex1i 5707

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3451   class class class wbr 5103  Rel wrel 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-rel 5658

This theorem is used by:  nprrel  5710  opeliunxp2  5815  ideqg  5829  issetid  5832  dffv2  6980  brfvopabrbr  6990  brrpssg  7741  opeliunxp2f  8227  brtpos2  8249  brdomg  8985  ctex  8990  isfi  9002  domssr  9026  domdifsn  9079  xpdom2  9091  xpdom1g  9093  sbth  9116  sdomirr  9133  sdomdif  9144  fodomr  9147  pwdom  9148  xpen  9159  pwen  9169  sbthfi  9214  sucdom2  9218  fineqv  9258  infsdomnn  9293  relprcnfsupp  9356  fsuppssov1  9376  fsuppunbi  9381  mapfien2  9401  harword  9557  brwdom  9561  domwdom  9568  brwdom3i  9577  unwdomg  9578  xpwdomg  9579  infdifsn  9658  ac10ct  10113  inffien  10142  djuen  10248  djudom2  10262  djufi  10265  cdainflem  10266  djulepw  10271  infdjuabs  10283  infunabs  10284  infmap2  10295  cfslb2n  10346  fin4i  10376  isfin5  10377  isfin6  10378  fin4en1  10387  isfin4p1  10393  isfin32i  10443  fin45  10470  fin56  10471  fin67  10473  hsmexlem1  10504  hsmexlem3  10506  axcc3  10516  ttukeylem1  10587  brdom3  10607  iundom2g  10624  iundom  10626  gchi  10709  engch  10713  gchdomtri  10714  fpwwe2lem5  10720  fpwwe2lem6  10721  fpwwe2lem8  10723  gchdjuidm  10753  gchpwdom  10755  prcdnq  11078  reexALT  13112  hasheni  14492  hashdomi  14524  climcl  15666  climi  15677  climrlim2  15714  climrecl  15750  climge0  15751  iseralt  15852  climfsum  15987  structex  17328  issubc  18010  pmtrfv  19666  dprdval  20219  frgpcyg  21879  lindff  22121  lindfind  22122  f1lindf  22128  lindfmm  22133  lsslindf  22136  lbslcic  22147  psrbaglesupp  22230  hauspwdom  23820  refbas  23829  refssex  23830  reftr  23833  refun0  23834  ovoliunnul  25828  dvle  26327  cyclnspth  30389  hlimi  31790  gsumhashmul  33628  extdgval  34285  finextfldext  34296  kardenir  35826  karddom  35829  kardsdom  35830  usgrgt2cycl  35909  brsset  36651  brbigcup  36660  elfix2  36666  brcolinear2  36823  isfne  37127  refssfne  37146  bj-epelg  37983  bj-ideqb  38080  bj-opelidb1ALT  38087  ovoliunnfl  38580  voliunnfl  38582  volsupnfl  38583  brabg2  38651  heiborlem4  38748  isrngo  38831  isdivrngo  38884  brssr  39513  issetssr  39515  fphpd  43822  ctbnfien  43824  sdomne0  44413  climd  46681  climuzlem  46752  rlimdmafv  48246  rlimdmafv2  48327  imasubc  50258  imassc  50260  imaid  50261  imaf1co  50262  imasubc3  50263  fuco112  50436  fuco111  50437  fuco21  50443  fucoid  50455