Theorem brrelex1i 5725

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

Syntax hints:   → wi 4   ∈ wcel 2098  Vcvv 3468   class class class wbr 5141  Rel wrel 5674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pr 5420

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-br 5142  df-opab 5204  df-xp 5675  df-rel 5676

This theorem is referenced by:  nprrel  5728  opeliunxp2  5832  ideqg  5845  issetid  5848  dffv2  6980  brfvopabrbr  6989  brrpssg  7712  opeliunxp2f  8196  brtpos2  8218  brdomg  8954  brdomgOLD  8955  ctex  8961  isfi  8974  domssr  8997  en1unielOLD  9031  domdifsn  9056  undomOLD  9062  xpdom2  9069  xpdom1g  9071  sucdom2OLD  9084  sbth  9095  dom0OLD  9105  sdom0OLD  9111  sdomirr  9116  sdomdif  9127  fodomr  9130  pwdom  9131  xpen  9142  pwen  9152  sbthfi  9204  sucdom2  9208  php3OLD  9226  sdom1OLD  9245  fineqv  9265  f1finf1oOLD  9274  infsdomnn  9307  infsdomnnOLD  9308  relprcnfsupp  9366  fsuppunbi  9386  mapfien2  9406  harword  9560  brwdom  9564  domwdom  9571  brwdom3i  9580  unwdomg  9581  xpwdomg  9582  infdifsn  9654  ac10ct  10031  inffien  10060  djuen  10166  djudom2  10180  djufi  10183  cdainflem  10184  djulepw  10189  infdjuabs  10203  infunabs  10204  infmap2  10215  cfslb2n  10265  fin4i  10295  isfin5  10296  isfin6  10297  fin4en1  10306  isfin4p1  10312  isfin32i  10362  fin45  10389  fin56  10390  fin67  10392  hsmexlem1  10423  hsmexlem3  10425  axcc3  10435  ttukeylem1  10506  brdom3  10525  iundom2g  10537  iundom  10539  gchi  10621  engch  10625  gchdomtri  10626  fpwwe2lem5  10632  fpwwe2lem6  10633  fpwwe2lem8  10635  gchdjuidm  10665  gchpwdom  10667  prcdnq  10990  reexALT  12972  hasheni  14313  hashdomi  14345  climcl  15449  climi  15460  climrlim2  15497  climrecl  15533  climge0  15534  iseralt  15637  climfsum  15772  structex  17092  issubc  17794  pmtrfv  19372  dprdval  19925  frgpcyg  21468  lindff  21710  lindfind  21711  f1lindf  21717  lindfmm  21722  lsslindf  21725  lbslcic  21736  psrbaglesupp  21818  hauspwdom  23360  refbas  23369  refssex  23370  reftr  23373  refun0  23374  ovoliunnul  25391  dvle  25895  cyclnspth  29566  hlimi  30950  gsumhashmul  32714  extdgval  33251  usgrgt2cycl  34649  brsset  35394  brbigcup  35403  elfix2  35409  brcolinear2  35563  isfne  35732  refssfne  35751  bj-epelg  36456  bj-ideqb  36547  bj-opelidb1ALT  36554  ovoliunnfl  37043  voliunnfl  37045  volsupnfl  37046  brabg2  37098  heiborlem4  37195  isrngo  37278  isdivrngo  37331  brssr  37884  issetssr  37886  fphpd  42132  ctbnfien  42134  sdomne0  42740  climd  44960  climuzlem  45031  rlimdmafv  46457  rlimdmafv2  46538