Theorem brrelex1i 5642

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3430   class class class wbr 5078  Rel wrel 5593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-opab 5141  df-xp 5594  df-rel 5595

This theorem is referenced by:  nprrel  5645  opeliunxp2  5744  ideqg  5757  issetid  5760  dffv2  6857  brfvopabrbr  6866  brrpssg  7569  opeliunxp2f  8010  brtpos2  8032  brdomg  8719  ctex  8724  isfi  8735  en1unielOLD  8789  domdifsn  8811  undom  8816  xpdom2  8823  xpdom1g  8825  sucdom2  8838  sbth  8849  dom0  8857  sdom0  8861  sdomirr  8866  sdomdif  8877  fodomr  8880  pwdom  8881  xpen  8892  pwen  8902  sbthfi  8950  php3OLD  8972  sdom1  8984  fineqv  8999  f1finf1o  9007  infsdomnn  9036  relprcnfsupp  9092  fsuppunbi  9110  mapfien2  9129  harword  9283  brwdom  9287  domwdom  9294  brwdom3i  9303  unwdomg  9304  xpwdomg  9305  infdifsn  9376  ac10ct  9774  inffien  9803  djuen  9909  djudom2  9923  djufi  9926  cdainflem  9927  djulepw  9932  infdjuabs  9946  infunabs  9947  infmap2  9958  cfslb2n  10008  fin4i  10038  isfin5  10039  isfin6  10040  fin4en1  10049  isfin4p1  10055  isfin32i  10105  fin45  10132  fin56  10133  fin67  10135  hsmexlem1  10166  hsmexlem3  10168  axcc3  10178  ttukeylem1  10249  brdom3  10268  iundom2g  10280  iundom  10282  gchi  10364  engch  10368  gchdomtri  10369  fpwwe2lem5  10375  fpwwe2lem6  10376  fpwwe2lem8  10378  gchdjuidm  10408  gchpwdom  10410  prcdnq  10733  reexALT  12706  hasheni  14043  hashdomi  14076  climcl  15189  climi  15200  climrlim2  15237  climrecl  15273  climge0  15274  iseralt  15377  climfsum  15513  structex  16832  issubc  17531  pmtrfv  19041  dprdval  19587  frgpcyg  20762  lindff  21003  lindfind  21004  f1lindf  21010  lindfmm  21015  lsslindf  21018  lbslcic  21029  psrbaglesupp  21108  hauspwdom  22633  refbas  22642  refssex  22643  reftr  22646  refun0  22647  ovoliunnul  24652  dvle  25152  cyclnspth  28147  hlimi  29529  gsumhashmul  31295  extdgval  31708  usgrgt2cycl  33071  brsset  34170  brbigcup  34179  elfix2  34185  brcolinear2  34339  isfne  34507  refssfne  34526  bj-epelg  35218  bj-ideqb  35309  bj-opelidb1ALT  35316  ovoliunnfl  35798  voliunnfl  35800  volsupnfl  35801  brabg2  35853  heiborlem4  35951  isrngo  36034  isdivrngo  36087  brssr  36598  issetssr  36600  fphpd  40618  ctbnfien  40620  climd  43167  climuzlem  43238  rlimdmafv  44620  rlimdmafv2  44701