Theorem brrelex1i 5693

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3446   class class class wbr 5110  Rel wrel 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-xp 5644  df-rel 5645

This theorem is referenced by:  nprrel  5696  opeliunxp2  5799  ideqg  5812  issetid  5815  dffv2  6941  brfvopabrbr  6950  brrpssg  7667  opeliunxp2f  8146  brtpos2  8168  brdomg  8903  brdomgOLD  8904  ctex  8910  isfi  8923  domssr  8946  en1unielOLD  8980  domdifsn  9005  undomOLD  9011  xpdom2  9018  xpdom1g  9020  sucdom2OLD  9033  sbth  9044  dom0OLD  9054  sdom0OLD  9060  sdomirr  9065  sdomdif  9076  fodomr  9079  pwdom  9080  xpen  9091  pwen  9101  sbthfi  9153  sucdom2  9157  php3OLD  9175  sdom1OLD  9194  fineqv  9214  f1finf1oOLD  9223  infsdomnn  9256  infsdomnnOLD  9257  relprcnfsupp  9315  fsuppunbi  9335  mapfien2  9354  harword  9508  brwdom  9512  domwdom  9519  brwdom3i  9528  unwdomg  9529  xpwdomg  9530  infdifsn  9602  ac10ct  9979  inffien  10008  djuen  10114  djudom2  10128  djufi  10131  cdainflem  10132  djulepw  10137  infdjuabs  10151  infunabs  10152  infmap2  10163  cfslb2n  10213  fin4i  10243  isfin5  10244  isfin6  10245  fin4en1  10254  isfin4p1  10260  isfin32i  10310  fin45  10337  fin56  10338  fin67  10340  hsmexlem1  10371  hsmexlem3  10373  axcc3  10383  ttukeylem1  10454  brdom3  10473  iundom2g  10485  iundom  10487  gchi  10569  engch  10573  gchdomtri  10574  fpwwe2lem5  10580  fpwwe2lem6  10581  fpwwe2lem8  10583  gchdjuidm  10613  gchpwdom  10615  prcdnq  10938  reexALT  12918  hasheni  14258  hashdomi  14290  climcl  15393  climi  15404  climrlim2  15441  climrecl  15477  climge0  15478  iseralt  15581  climfsum  15716  structex  17033  issubc  17735  pmtrfv  19248  dprdval  19796  frgpcyg  21017  lindff  21258  lindfind  21259  f1lindf  21265  lindfmm  21270  lsslindf  21273  lbslcic  21284  psrbaglesupp  21363  hauspwdom  22889  refbas  22898  refssex  22899  reftr  22902  refun0  22903  ovoliunnul  24908  dvle  25408  cyclnspth  28811  hlimi  30193  gsumhashmul  31968  extdgval  32430  usgrgt2cycl  33811  brsset  34550  brbigcup  34559  elfix2  34565  brcolinear2  34719  isfne  34887  refssfne  34906  bj-epelg  35612  bj-ideqb  35703  bj-opelidb1ALT  35710  ovoliunnfl  36193  voliunnfl  36195  volsupnfl  36196  brabg2  36248  heiborlem4  36346  isrngo  36429  isdivrngo  36482  brssr  37036  issetssr  37038  fphpd  41197  ctbnfien  41199  sdomne0  41807  climd  44033  climuzlem  44104  rlimdmafv  45529  rlimdmafv2  45610