Theorem brrelex1i 5608

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3494   class class class wbr 5066  Rel wrel 5560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-xp 5561  df-rel 5562

This theorem is referenced by:  nprrel  5611  opeliunxp2  5709  ideqg  5722  issetid  5725  dffv2  6756  brfvopabrbr  6765  brrpssg  7451  opeliunxp2f  7876  brtpos2  7898  brdomg  8519  ctex  8524  isfi  8533  en1uniel  8581  domdifsn  8600  undom  8605  xpdom2  8612  xpdom1g  8614  sbth  8637  dom0  8645  sdom0  8649  sdomirr  8654  sdomdif  8665  fodomr  8668  pwdom  8669  xpen  8680  pwen  8690  php3  8703  sucdom2  8714  sdom1  8718  fineqv  8733  f1finf1o  8745  infsdomnn  8779  relprcnfsupp  8836  fsuppunbi  8854  mapfien2  8872  harword  9029  brwdom  9031  domwdom  9038  brwdom3i  9047  unwdomg  9048  xpwdomg  9049  infdifsn  9120  ac10ct  9460  inffien  9489  djuen  9595  djudom2  9609  djufi  9612  cdainflem  9613  djulepw  9618  infdjuabs  9628  infunabs  9629  infmap2  9640  cfslb2n  9690  fin4i  9720  isfin5  9721  isfin6  9722  fin4en1  9731  isfin4p1  9737  isfin32i  9787  fin45  9814  fin56  9815  fin67  9817  hsmexlem1  9848  hsmexlem3  9850  axcc3  9860  ttukeylem1  9931  brdom3  9950  iundom2g  9962  iundom  9964  gchi  10046  engch  10050  gchdomtri  10051  fpwwe2lem6  10057  fpwwe2lem7  10058  fpwwe2lem9  10060  gchdjuidm  10090  gchpwdom  10092  prcdnq  10415  reexALT  12384  hasheni  13709  hashdomi  13742  brfi1indALT  13859  climcl  14856  climi  14867  climrlim2  14904  climrecl  14940  climge0  14941  iseralt  15041  climfsum  15175  structex  16494  issubc  17105  pmtrfv  18580  dprdval  19125  frgpcyg  20720  lindff  20959  lindfind  20960  f1lindf  20966  lindfmm  20971  lsslindf  20974  lbslcic  20985  hauspwdom  22109  refbas  22118  refssex  22119  reftr  22122  refun0  22123  ovoliunnul  24108  dvle  24604  cyclnspth  27581  hlimi  28965  extdgval  31044  usgrgt2cycl  32377  brsset  33350  brbigcup  33359  elfix2  33365  brcolinear2  33519  isfne  33687  refssfne  33706  bj-epelg  34363  bj-ideqb  34454  bj-opelidb1ALT  34461  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  brabg2  35006  heiborlem4  35107  isrngo  35190  isdivrngo  35243  brssr  35756  issetssr  35758  fphpd  39433  ctbnfien  39435  climd  41973  climuzlem  42044  rlimdmafv  43396  rlimdmafv2  43477