Theorem brrelexi 5072

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

Proof of Theorem brrelexi

Step	Hyp	Ref	Expression
1		brrelexi.1	. 2 ⊢ Rel 𝑅
2		brrelex 5070	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
3	1, 2	mpan 701	1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 1976  Vcvv 3172   class class class wbr 4577  Rel wrel 5033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578  df-opab 4638  df-xp 5034  df-rel 5035

This theorem is referenced by:  nprrel  5074  vtoclr  5076  opeliunxp2  5170  ideqg  5183  issetid  5186  dffv2  6166  brrpssg  6815  opeliunxp2f  7201  brtpos2  7223  brdomg  7829  isfi  7843  en1uniel  7892  domdifsn  7906  undom  7911  xpdom2  7918  xpdom1g  7920  sbth  7943  dom0  7951  sdom0  7955  sdomirr  7960  sdomdif  7971  fodomr  7974  pwdom  7975  xpen  7986  pwen  7996  php3  8009  sucdom2  8019  sdom1  8023  fineqv  8038  f1finf1o  8050  infsdomnn  8084  relprcnfsupp  8139  fsuppimp  8142  fsuppunbi  8157  mapfien2  8175  harword  8331  brwdom  8333  domwdom  8340  brwdom3i  8349  unwdomg  8350  xpwdomg  8351  infdifsn  8415  ac10ct  8718  inffien  8747  iunfictbso  8798  cdaen  8856  cdadom1  8869  cdafi  8873  cdainflem  8874  cdalepw  8879  unctb  8888  infcdaabs  8889  infunabs  8890  infmap2  8901  cfslb2n  8951  fin4i  8981  isfin5  8982  isfin6  8983  fin4en1  8992  isfin4-3  8998  isfin32i  9048  fin45  9075  fin56  9076  fin67  9078  hsmexlem1  9109  hsmexlem3  9111  axcc3  9121  ttukeylem1  9192  brdom3  9209  iundom2g  9219  iundom  9221  iunctb  9253  gchi  9303  engch  9307  gchdomtri  9308  fpwwe2lem6  9314  fpwwe2lem7  9315  fpwwe2lem9  9317  gchpwdom  9349  prcdnq  9672  reexALT  11661  hasheni  12953  hashdomi  12985  brfi1indALT  13086  brfi1indALTOLD  13092  climcl  14027  climi  14038  climrlim2  14075  climrecl  14111  climge0  14112  iseralt  14212  climfsum  14342  strfv  15684  issubc  16267  pmtrfv  17644  dprdval  18174  cnfldex  19519  frgpcyg  19689  lindff  19921  lindfind  19922  f1lindf  19928  lindfmm  19933  lsslindf  19936  lbslcic  19947  1stcrestlem  21013  2ndcdisj2  21018  dis2ndc  21021  hauspwdom  21062  refbas  21071  refssex  21072  reftr  21075  refun0  21076  ovoliunnul  23027  uniiccdif  23097  dvle  23519  uhgrav  25619  ushgraf  25625  ushgrauhgra  25626  umgraf2  25640  umgrares  25647  umisuhgra  25650  uslgrav  25660  usgrav  25661  uslgraf  25668  iscusgra0  25780  eupap1  26297  eupath2lem3  26300  eupath2  26301  frisusgrapr  26312  hlimi  27263  brsset  31000  brbigcup  31009  elfix2  31015  brcolinear2  31169  isfne  31338  refssfne  31357  ovoliunnfl  32445  voliunnfl  32447  volsupnfl  32448  brabg2  32504  heiborlem4  32607  isrngo  32690  isdivrngo  32743  fphpd  36222  ctbnfien  36224  climd  38563  rlimdmafv  39731  subgrv  40516  linindsv  42050