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 690	1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3436   class class class wbr 5092  Rel wrel 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-xp 5625  df-rel 5626

This theorem is referenced by:  nprrel  5678  opeliunxp2  5781  ideqg  5794  issetid  5797  dffv2  6918  brfvopabrbr  6927  brrpssg  7661  opeliunxp2f  8143  brtpos2  8165  brdomg  8884  ctex  8889  isfi  8901  domssr  8924  domdifsn  8977  xpdom2  8989  xpdom1g  8991  sbth  9014  sdomirr  9031  sdomdif  9042  fodomr  9045  pwdom  9046  xpen  9057  pwen  9067  sbthfi  9113  sucdom2  9117  fineqv  9156  infsdomnn  9190  relprcnfsupp  9254  fsuppssov1  9274  fsuppunbi  9279  mapfien2  9299  harword  9455  brwdom  9459  domwdom  9466  brwdom3i  9475  unwdomg  9476  xpwdomg  9477  infdifsn  9553  ac10ct  9928  inffien  9957  djuen  10064  djudom2  10078  djufi  10081  cdainflem  10082  djulepw  10087  infdjuabs  10099  infunabs  10100  infmap2  10111  cfslb2n  10162  fin4i  10192  isfin5  10193  isfin6  10194  fin4en1  10203  isfin4p1  10209  isfin32i  10259  fin45  10286  fin56  10287  fin67  10289  hsmexlem1  10320  hsmexlem3  10322  axcc3  10332  ttukeylem1  10403  brdom3  10422  iundom2g  10434  iundom  10436  gchi  10518  engch  10522  gchdomtri  10523  fpwwe2lem5  10529  fpwwe2lem6  10530  fpwwe2lem8  10532  gchdjuidm  10562  gchpwdom  10564  prcdnq  10887  reexALT  12885  hasheni  14255  hashdomi  14287  climcl  15406  climi  15417  climrlim2  15454  climrecl  15490  climge0  15491  iseralt  15592  climfsum  15727  structex  17061  issubc  17742  pmtrfv  19331  dprdval  19884  frgpcyg  21480  lindff  21722  lindfind  21723  f1lindf  21729  lindfmm  21734  lsslindf  21737  lbslcic  21748  psrbaglesupp  21829  hauspwdom  23386  refbas  23395  refssex  23396  reftr  23399  refun0  23400  ovoliunnul  25406  dvle  25910  cyclnspth  29746  hlimi  31132  gsumhashmul  33015  extdgval  33626  finextfldext  33637  usgrgt2cycl  35113  brsset  35873  brbigcup  35882  elfix2  35888  brcolinear2  36042  isfne  36323  refssfne  36342  bj-epelg  37052  bj-ideqb  37143  bj-opelidb1ALT  37150  ovoliunnfl  37652  voliunnfl  37654  volsupnfl  37655  brabg2  37707  heiborlem4  37804  isrngo  37887  isdivrngo  37940  brssr  38488  issetssr  38490  fphpd  42799  ctbnfien  42801  sdomne0  43396  climd  45663  climuzlem  45734  rlimdmafv  47171  rlimdmafv2  47252  imasubc  49146  imassc  49148  imaid  49149  imaf1co  49150  imasubc3  49151  fuco112  49324  fuco111  49325  fuco21  49331  fucoid  49343