Theorem brrelex1i 5731

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

Syntax hints:   → wi 4   ∈ wcel 2104  Vcvv 3472   class class class wbr 5147  Rel wrel 5680

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 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-rel 5682

This theorem is referenced by:  nprrel  5734  opeliunxp2  5837  ideqg  5850  issetid  5853  dffv2  6985  brfvopabrbr  6994  brrpssg  7717  opeliunxp2f  8197  brtpos2  8219  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  14312  hashdomi  14344  climcl  15447  climi  15458  climrlim2  15495  climrecl  15531  climge0  15532  iseralt  15635  climfsum  15770  structex  17087  issubc  17789  pmtrfv  19361  dprdval  19914  frgpcyg  21348  lindff  21589  lindfind  21590  f1lindf  21596  lindfmm  21601  lsslindf  21604  lbslcic  21615  psrbaglesupp  21696  hauspwdom  23225  refbas  23234  refssex  23235  reftr  23238  refun0  23239  ovoliunnul  25256  dvle  25759  cyclnspth  29324  hlimi  30708  gsumhashmul  32478  extdgval  33021  usgrgt2cycl  34419  brsset  35165  brbigcup  35174  elfix2  35180  brcolinear2  35334  isfne  35527  refssfne  35546  bj-epelg  36252  bj-ideqb  36343  bj-opelidb1ALT  36350  ovoliunnfl  36833  voliunnfl  36835  volsupnfl  36836  brabg2  36888  heiborlem4  36985  isrngo  37068  isdivrngo  37121  brssr  37674  issetssr  37676  fphpd  41856  ctbnfien  41858  sdomne0  42466  climd  44686  climuzlem  44757  rlimdmafv  46183  rlimdmafv2  46264