Theorem brrelex1i 5682

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430   class class class wbr 5086  Rel wrel 5631

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5632  df-rel 5633

This theorem is referenced by:  nprrel  5685  opeliunxp2  5789  ideqg  5802  issetid  5805  dffv2  6931  brfvopabrbr  6940  brrpssg  7674  opeliunxp2f  8155  brtpos2  8177  brdomg  8900  ctex  8905  isfi  8917  domssr  8941  domdifsn  8993  xpdom2  9005  xpdom1g  9007  sbth  9030  sdomirr  9047  sdomdif  9058  fodomr  9061  pwdom  9062  xpen  9073  pwen  9083  sbthfi  9128  sucdom2  9132  fineqv  9172  infsdomnn  9206  relprcnfsupp  9272  fsuppssov1  9292  fsuppunbi  9297  mapfien2  9317  harword  9473  brwdom  9477  domwdom  9484  brwdom3i  9493  unwdomg  9494  xpwdomg  9495  infdifsn  9573  ac10ct  9951  inffien  9980  djuen  10087  djudom2  10101  djufi  10104  cdainflem  10105  djulepw  10110  infdjuabs  10122  infunabs  10123  infmap2  10134  cfslb2n  10185  fin4i  10215  isfin5  10216  isfin6  10217  fin4en1  10226  isfin4p1  10232  isfin32i  10282  fin45  10309  fin56  10310  fin67  10312  hsmexlem1  10343  hsmexlem3  10345  axcc3  10355  ttukeylem1  10426  brdom3  10445  iundom2g  10457  iundom  10459  gchi  10542  engch  10546  gchdomtri  10547  fpwwe2lem5  10553  fpwwe2lem6  10554  fpwwe2lem8  10556  gchdjuidm  10586  gchpwdom  10588  prcdnq  10911  reexALT  12929  hasheni  14305  hashdomi  14337  climcl  15456  climi  15467  climrlim2  15504  climrecl  15540  climge0  15541  iseralt  15642  climfsum  15778  structex  17115  issubc  17797  pmtrfv  19422  dprdval  19975  frgpcyg  21567  lindff  21809  lindfind  21810  f1lindf  21816  lindfmm  21821  lsslindf  21824  lbslcic  21835  psrbaglesupp  21916  hauspwdom  23480  refbas  23489  refssex  23490  reftr  23493  refun0  23494  ovoliunnul  25488  dvle  25988  cyclnspth  29888  hlimi  31278  gsumhashmul  33147  extdgval  33817  finextfldext  33828  usgrgt2cycl  35332  brsset  36089  brbigcup  36098  elfix2  36104  brcolinear2  36260  isfne  36541  refssfne  36560  bj-epelg  37395  bj-ideqb  37493  bj-opelidb1ALT  37500  ovoliunnfl  38001  voliunnfl  38003  volsupnfl  38004  brabg2  38056  heiborlem4  38153  isrngo  38236  isdivrngo  38289  brssr  38920  issetssr  38922  fphpd  43266  ctbnfien  43268  sdomne0  43862  climd  46122  climuzlem  46193  rlimdmafv  47641  rlimdmafv2  47722  imasubc  49642  imassc  49644  imaid  49645  imaf1co  49646  imasubc3  49647  fuco112  49820  fuco111  49821  fuco21  49827  fucoid  49839