Theorem brrelex1i 5690

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442   class class class wbr 5100  Rel wrel 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5245  ax-pr 5381

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5640  df-rel 5641

This theorem is referenced by:  nprrel  5693  opeliunxp2  5797  ideqg  5810  issetid  5813  dffv2  6939  brfvopabrbr  6948  brrpssg  7682  opeliunxp2f  8164  brtpos2  8186  brdomg  8909  ctex  8914  isfi  8926  domssr  8950  domdifsn  9002  xpdom2  9014  xpdom1g  9016  sbth  9039  sdomirr  9056  sdomdif  9067  fodomr  9070  pwdom  9071  xpen  9082  pwen  9092  sbthfi  9137  sucdom2  9141  fineqv  9181  infsdomnn  9215  relprcnfsupp  9281  fsuppssov1  9301  fsuppunbi  9306  mapfien2  9326  harword  9482  brwdom  9486  domwdom  9493  brwdom3i  9502  unwdomg  9503  xpwdomg  9504  infdifsn  9580  ac10ct  9958  inffien  9987  djuen  10094  djudom2  10108  djufi  10111  cdainflem  10112  djulepw  10117  infdjuabs  10129  infunabs  10130  infmap2  10141  cfslb2n  10192  fin4i  10222  isfin5  10223  isfin6  10224  fin4en1  10233  isfin4p1  10239  isfin32i  10289  fin45  10316  fin56  10317  fin67  10319  hsmexlem1  10350  hsmexlem3  10352  axcc3  10362  ttukeylem1  10433  brdom3  10452  iundom2g  10464  iundom  10466  gchi  10549  engch  10553  gchdomtri  10554  fpwwe2lem5  10560  fpwwe2lem6  10561  fpwwe2lem8  10563  gchdjuidm  10593  gchpwdom  10595  prcdnq  10918  reexALT  12911  hasheni  14285  hashdomi  14317  climcl  15436  climi  15447  climrlim2  15484  climrecl  15520  climge0  15521  iseralt  15622  climfsum  15757  structex  17091  issubc  17773  pmtrfv  19398  dprdval  19951  frgpcyg  21545  lindff  21787  lindfind  21788  f1lindf  21794  lindfmm  21799  lsslindf  21802  lbslcic  21813  psrbaglesupp  21895  hauspwdom  23462  refbas  23471  refssex  23472  reftr  23475  refun0  23476  ovoliunnul  25481  dvle  25985  cyclnspth  29892  hlimi  31282  gsumhashmul  33167  extdgval  33837  finextfldext  33848  usgrgt2cycl  35352  brsset  36109  brbigcup  36118  elfix2  36124  brcolinear2  36280  isfne  36561  refssfne  36580  bj-epelg  37343  bj-ideqb  37441  bj-opelidb1ALT  37448  ovoliunnfl  37942  voliunnfl  37944  volsupnfl  37945  brabg2  37997  heiborlem4  38094  isrngo  38177  isdivrngo  38230  brssr  38861  issetssr  38863  fphpd  43202  ctbnfien  43204  sdomne0  43798  climd  46059  climuzlem  46130  rlimdmafv  47566  rlimdmafv2  47647  imasubc  49539  imassc  49541  imaid  49542  imaf1co  49543  imasubc3  49544  fuco112  49717  fuco111  49718  fuco21  49724  fucoid  49736