Theorem brrelex1i 5728

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

Syntax hints:   → wi 4   ∈ wcel 2098  Vcvv 3463   class class class wbr 5143  Rel wrel 5677

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 2696  ax-sep 5294  ax-nul 5301  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3465  df-dif 3942  df-un 3944  df-ss 3956  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5144  df-opab 5206  df-xp 5678  df-rel 5679

This theorem is referenced by:  nprrel  5731  opeliunxp2  5835  ideqg  5848  issetid  5851  dffv2  6988  brfvopabrbr  6997  brrpssg  7728  opeliunxp2f  8214  brtpos2  8236  brdomg  8975  brdomgOLD  8976  ctex  8982  isfi  8995  domssr  9018  en1unielOLD  9052  domdifsn  9077  undomOLD  9083  xpdom2  9090  xpdom1g  9092  sucdom2OLD  9105  sbth  9116  dom0OLD  9126  sdom0OLD  9132  sdomirr  9137  sdomdif  9148  fodomr  9151  pwdom  9152  xpen  9163  pwen  9173  sbthfi  9225  sucdom2  9229  php3OLD  9247  sdom1OLD  9266  fineqv  9286  f1finf1oOLD  9295  infsdomnn  9328  infsdomnnOLD  9329  relprcnfsupp  9388  fsuppssov1  9407  fsuppunbi  9412  mapfien2  9432  harword  9586  brwdom  9590  domwdom  9597  brwdom3i  9606  unwdomg  9607  xpwdomg  9608  infdifsn  9680  ac10ct  10057  inffien  10086  djuen  10192  djudom2  10206  djufi  10209  cdainflem  10210  djulepw  10215  infdjuabs  10229  infunabs  10230  infmap2  10241  cfslb2n  10291  fin4i  10321  isfin5  10322  isfin6  10323  fin4en1  10332  isfin4p1  10338  isfin32i  10388  fin45  10415  fin56  10416  fin67  10418  hsmexlem1  10449  hsmexlem3  10451  axcc3  10461  ttukeylem1  10532  brdom3  10551  iundom2g  10563  iundom  10565  gchi  10647  engch  10651  gchdomtri  10652  fpwwe2lem5  10658  fpwwe2lem6  10659  fpwwe2lem8  10661  gchdjuidm  10691  gchpwdom  10693  prcdnq  11016  reexALT  12998  hasheni  14339  hashdomi  14371  climcl  15475  climi  15486  climrlim2  15523  climrecl  15559  climge0  15560  iseralt  15663  climfsum  15798  structex  17118  issubc  17820  pmtrfv  19411  dprdval  19964  frgpcyg  21511  lindff  21753  lindfind  21754  f1lindf  21760  lindfmm  21765  lsslindf  21768  lbslcic  21779  psrbaglesupp  21861  hauspwdom  23423  refbas  23432  refssex  23433  reftr  23436  refun0  23437  ovoliunnul  25454  dvle  25958  cyclnspth  29658  hlimi  31042  gsumhashmul  32815  extdgval  33403  usgrgt2cycl  34797  brsset  35542  brbigcup  35551  elfix2  35557  brcolinear2  35711  isfne  35880  refssfne  35899  bj-epelg  36604  bj-ideqb  36695  bj-opelidb1ALT  36702  ovoliunnfl  37192  voliunnfl  37194  volsupnfl  37195  brabg2  37247  heiborlem4  37344  isrngo  37427  isdivrngo  37480  brssr  38029  issetssr  38031  fphpd  42301  ctbnfien  42303  sdomne0  42908  climd  45123  climuzlem  45194  rlimdmafv  46620  rlimdmafv2  46701