Theorem brrelex1i 5717

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2143  Vcvv 3455   class class class wbr 5109  Rel wrel 5666

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-xp 5667  df-rel 5668

This theorem is used by:  nprrel  5720  opeliunxp2  5824  ideqg  5837  issetid  5840  dffv2  6976  brfvopabrbr  6986  brrpssg  7722  opeliunxp2f  8202  brtpos2  8224  brdomg  8951  ctex  8956  isfi  8968  domssr  8992  domdifsn  9044  xpdom2  9056  xpdom1g  9058  sbth  9081  sdomirr  9098  sdomdif  9109  fodomr  9112  pwdom  9113  xpen  9124  pwen  9134  sbthfi  9179  sucdom2  9183  fineqv  9223  infsdomnn  9257  relprcnfsupp  9320  fsuppssov1  9340  fsuppunbi  9345  mapfien2  9365  harword  9521  brwdom  9525  domwdom  9532  brwdom3i  9541  unwdomg  9542  xpwdomg  9543  infdifsn  9622  ac10ct  10023  inffien  10052  djuen  10158  djudom2  10172  djufi  10175  cdainflem  10176  djulepw  10181  infdjuabs  10193  infunabs  10194  infmap2  10205  cfslb2n  10256  fin4i  10286  isfin5  10287  isfin6  10288  fin4en1  10297  isfin4p1  10303  isfin32i  10353  fin45  10380  fin56  10381  fin67  10383  hsmexlem1  10414  hsmexlem3  10416  axcc3  10426  ttukeylem1  10497  brdom3  10516  iundom2g  10528  iundom  10530  gchi  10613  engch  10617  gchdomtri  10618  fpwwe2lem5  10624  fpwwe2lem6  10625  fpwwe2lem8  10627  gchdjuidm  10657  gchpwdom  10659  prcdnq  10982  reexALT  13012  hasheni  14389  hashdomi  14421  climcl  15555  climi  15566  climrlim2  15603  climrecl  15639  climge0  15640  iseralt  15741  climfsum  15877  structex  17214  issubc  17896  pmtrfv  19526  dprdval  20079  frgpcyg  21732  lindff  21974  lindfind  21975  f1lindf  21981  lindfmm  21986  lsslindf  21989  lbslcic  22000  psrbaglesupp  22081  hauspwdom  23667  refbas  23676  refssex  23677  reftr  23680  refun0  23681  ovoliunnul  25675  dvle  26175  cyclnspth  30159  hlimi  31549  gsumhashmul  33396  extdgval  34052  finextfldext  34063  kardenir  35579  karddom  35582  kardsdom  35583  usgrgt2cycl  35630  brsset  36387  brbigcup  36396  elfix2  36402  brcolinear2  36558  isfne  36878  refssfne  36897  bj-epelg  37732  bj-ideqb  37831  bj-opelidb1ALT  37838  ovoliunnfl  38341  voliunnfl  38343  volsupnfl  38344  brabg2  38396  heiborlem4  38493  isrngo  38576  isdivrngo  38629  brssr  39258  issetssr  39260  fphpd  43571  ctbnfien  43573  sdomne0  44167  climd  46414  climuzlem  46485  rlimdmafv  47942  rlimdmafv2  48023  imasubc  49957  imassc  49959  imaid  49960  imaf1co  49961  imasubc3  49962  fuco112  50135  fuco111  50136  fuco21  50142  fucoid  50154