Theorem brrelex1i 5676

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

Syntax hints:   → wi 4   ∈ wcel 2121  Vcvv 3433   class class class wbr 5074  Rel wrel 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5220  ax-pr 5364

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075  df-opab 5137  df-xp 5626  df-rel 5627

This theorem is referenced by:  nprrel  5679  opeliunxp2  5782  ideqg  5795  issetid  5798  dffv2  6925  brfvopabrbr  6935  brrpssg  7671  opeliunxp2f  8152  brtpos2  8174  brdomg  8899  ctex  8904  isfi  8916  domssr  8940  domdifsn  8992  xpdom2  9004  xpdom1g  9006  sbth  9029  sdomirr  9046  sdomdif  9057  fodomr  9060  pwdom  9061  xpen  9072  pwen  9082  sbthfi  9127  sucdom2  9131  fineqv  9171  infsdomnn  9205  relprcnfsupp  9271  fsuppssov1  9291  fsuppunbi  9296  mapfien2  9316  harword  9472  brwdom  9476  domwdom  9483  brwdom3i  9492  unwdomg  9493  xpwdomg  9494  infdifsn  9573  ac10ct  9951  inffien  9980  djuen  10087  djudom2  10101  djufi  10104  cdainflem  10105  djulepw  10110  infdjuabs  10122  infunabs  10123  infmap2  10134  cfslb2n  10186  fin4i  10216  isfin5  10217  isfin6  10218  fin4en1  10227  isfin4p1  10233  isfin32i  10283  fin45  10310  fin56  10311  fin67  10313  hsmexlem1  10344  hsmexlem3  10346  axcc3  10356  ttukeylem1  10427  brdom3  10446  iundom2g  10458  iundom  10460  gchi  10543  engch  10547  gchdomtri  10548  fpwwe2lem5  10554  fpwwe2lem6  10555  fpwwe2lem8  10557  gchdjuidm  10587  gchpwdom  10589  prcdnq  10912  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  19421  dprdval  19974  frgpcyg  21551  lindff  21793  lindfind  21794  f1lindf  21800  lindfmm  21805  lsslindf  21808  lbslcic  21819  psrbaglesupp  21900  hauspwdom  23487  refbas  23496  refssex  23497  reftr  23500  refun0  23501  ovoliunnul  25495  dvle  25995  cyclnspth  29889  hlimi  31279  gsumhashmul  33150  extdgval  33847  finextfldext  33858  usgrgt2cycl  35371  brsset  36128  brbigcup  36137  elfix2  36143  brcolinear2  36299  isfne  36580  refssfne  36599  bj-epelg  37434  bj-ideqb  37532  bj-opelidb1ALT  37539  ovoliunnfl  38042  voliunnfl  38044  volsupnfl  38045  brabg2  38097  heiborlem4  38194  isrngo  38277  isdivrngo  38330  brssr  38961  issetssr  38963  fphpd  43274  ctbnfien  43276  sdomne0  43870  climd  46127  climuzlem  46198  rlimdmafv  47652  rlimdmafv2  47733  imasubc  49653  imassc  49655  imaid  49656  imaf1co  49657  imasubc3  49658  fuco112  49831  fuco111  49832  fuco21  49838  fucoid  49850