Theorem brrelex1i 5744

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3477   class class class wbr 5147  Rel wrel 5693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-rel 5695

This theorem is referenced by:  nprrel  5747  opeliunxp2  5851  ideqg  5864  issetid  5867  dffv2  7003  brfvopabrbr  7012  brrpssg  7743  opeliunxp2f  8233  brtpos2  8255  brdomg  8995  brdomgOLD  8996  ctex  9002  isfi  9014  domssr  9037  domdifsn  9092  undomOLD  9098  xpdom2  9105  xpdom1g  9107  sucdom2OLD  9120  sbth  9131  dom0OLD  9141  sdom0OLD  9147  sdomirr  9152  sdomdif  9163  fodomr  9166  pwdom  9167  xpen  9178  pwen  9188  sbthfi  9236  sucdom2  9240  php3OLD  9258  sdom1OLD  9276  fineqv  9296  f1finf1oOLD  9303  infsdomnn  9335  infsdomnnOLD  9336  relprcnfsupp  9401  fsuppssov1  9421  fsuppunbi  9426  mapfien2  9446  harword  9600  brwdom  9604  domwdom  9611  brwdom3i  9620  unwdomg  9621  xpwdomg  9622  infdifsn  9694  ac10ct  10071  inffien  10100  djuen  10207  djudom2  10221  djufi  10224  cdainflem  10225  djulepw  10230  infdjuabs  10242  infunabs  10243  infmap2  10254  cfslb2n  10305  fin4i  10335  isfin5  10336  isfin6  10337  fin4en1  10346  isfin4p1  10352  isfin32i  10402  fin45  10429  fin56  10430  fin67  10432  hsmexlem1  10463  hsmexlem3  10465  axcc3  10475  ttukeylem1  10546  brdom3  10565  iundom2g  10577  iundom  10579  gchi  10661  engch  10665  gchdomtri  10666  fpwwe2lem5  10672  fpwwe2lem6  10673  fpwwe2lem8  10675  gchdjuidm  10705  gchpwdom  10707  prcdnq  11030  reexALT  13023  hasheni  14383  hashdomi  14415  climcl  15531  climi  15542  climrlim2  15579  climrecl  15615  climge0  15616  iseralt  15717  climfsum  15852  structex  17183  issubc  17885  pmtrfv  19484  dprdval  20037  frgpcyg  21609  lindff  21852  lindfind  21853  f1lindf  21859  lindfmm  21864  lsslindf  21867  lbslcic  21878  psrbaglesupp  21959  hauspwdom  23524  refbas  23533  refssex  23534  reftr  23537  refun0  23538  ovoliunnul  25555  dvle  26060  cyclnspth  29832  hlimi  31216  gsumhashmul  33046  extdgval  33681  usgrgt2cycl  35114  brsset  35870  brbigcup  35879  elfix2  35885  brcolinear2  36039  isfne  36321  refssfne  36340  bj-epelg  37050  bj-ideqb  37141  bj-opelidb1ALT  37148  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  brabg2  37703  heiborlem4  37800  isrngo  37883  isdivrngo  37936  brssr  38482  issetssr  38484  fphpd  42803  ctbnfien  42805  sdomne0  43402  climd  45627  climuzlem  45698  rlimdmafv  47126  rlimdmafv2  47207