Theorem brrelex1i 5675

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

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3431   class class class wbr 5073  Rel wrel 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5219  ax-pr 5363

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4263  df-if 4456  df-sn 4557  df-pr 4559  df-op 4563  df-br 5074  df-opab 5136  df-xp 5625  df-rel 5626

This theorem is referenced by:  nprrel  5678  opeliunxp2  5781  ideqg  5794  issetid  5797  dffv2  6923  brfvopabrbr  6933  brrpssg  7669  opeliunxp2f  8151  brtpos2  8173  brdomg  8896  ctex  8901  isfi  8913  domssr  8937  domdifsn  8989  xpdom2  9001  xpdom1g  9003  sbth  9026  sdomirr  9043  sdomdif  9054  fodomr  9057  pwdom  9058  xpen  9069  pwen  9079  sbthfi  9124  sucdom2  9128  fineqv  9168  infsdomnn  9202  relprcnfsupp  9268  fsuppssov1  9288  fsuppunbi  9293  mapfien2  9313  harword  9469  brwdom  9473  domwdom  9480  brwdom3i  9489  unwdomg  9490  xpwdomg  9491  infdifsn  9570  ac10ct  9948  inffien  9977  djuen  10084  djudom2  10098  djufi  10101  cdainflem  10102  djulepw  10107  infdjuabs  10119  infunabs  10120  infmap2  10131  cfslb2n  10182  fin4i  10212  isfin5  10213  isfin6  10214  fin4en1  10223  isfin4p1  10229  isfin32i  10279  fin45  10306  fin56  10307  fin67  10309  hsmexlem1  10340  hsmexlem3  10342  axcc3  10352  ttukeylem1  10423  brdom3  10442  iundom2g  10454  iundom  10456  gchi  10539  engch  10543  gchdomtri  10544  fpwwe2lem5  10550  fpwwe2lem6  10551  fpwwe2lem8  10553  gchdjuidm  10583  gchpwdom  10585  prcdnq  10908  reexALT  12926  hasheni  14302  hashdomi  14334  climcl  15453  climi  15464  climrlim2  15501  climrecl  15537  climge0  15538  iseralt  15639  climfsum  15775  structex  17112  issubc  17794  pmtrfv  19419  dprdval  19972  frgpcyg  21549  lindff  21791  lindfind  21792  f1lindf  21798  lindfmm  21803  lsslindf  21806  lbslcic  21817  psrbaglesupp  21898  hauspwdom  23485  refbas  23494  refssex  23495  reftr  23498  refun0  23499  ovoliunnul  25493  dvle  25993  cyclnspth  29888  hlimi  31278  gsumhashmul  33149  extdgval  33846  finextfldext  33857  usgrgt2cycl  35367  brsset  36124  brbigcup  36133  elfix2  36139  brcolinear2  36295  isfne  36576  refssfne  36595  bj-epelg  37430  bj-ideqb  37528  bj-opelidb1ALT  37535  ovoliunnfl  38038  voliunnfl  38040  volsupnfl  38041  brabg2  38093  heiborlem4  38190  isrngo  38273  isdivrngo  38326  brssr  38957  issetssr  38959  fphpd  43270  ctbnfien  43272  sdomne0  43866  climd  46123  climuzlem  46194  rlimdmafv  47648  rlimdmafv2  47729  imasubc  49649  imassc  49651  imaid  49652  imaf1co  49653  imasubc3  49654  fuco112  49827  fuco111  49828  fuco21  49834  fucoid  49846