Theorem brrelexi 5192

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

Syntax hints:   → wi 4   ∈ wcel 2030  Vcvv 3231   class class class wbr 4685  Rel wrel 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-xp 5149  df-rel 5150

This theorem is referenced by:  nprrel  5195  vtoclr  5198  opeliunxp2  5293  ideqg  5306  issetid  5309  dffv2  6310  brfvopabrbr  6318  brrpssg  6981  opeliunxp2f  7381  brtpos2  7403  brdomg  8007  isfi  8021  en1uniel  8069  domdifsn  8084  undom  8089  xpdom2  8096  xpdom1g  8098  sbth  8121  dom0  8129  sdom0  8133  sdomirr  8138  sdomdif  8149  fodomr  8152  pwdom  8153  xpen  8164  pwen  8174  php3  8187  sucdom2  8197  sdom1  8201  fineqv  8216  f1finf1o  8228  infsdomnn  8262  relprcnfsupp  8319  fsuppimp  8322  fsuppunbi  8337  mapfien2  8355  harword  8511  brwdom  8513  domwdom  8520  brwdom3i  8529  unwdomg  8530  xpwdomg  8531  infdifsn  8592  ac10ct  8895  inffien  8924  iunfictbso  8975  cdaen  9033  cdadom1  9046  cdafi  9050  cdainflem  9051  cdalepw  9056  unctb  9065  infcdaabs  9066  infunabs  9067  infmap2  9078  cfslb2n  9128  fin4i  9158  isfin5  9159  isfin6  9160  fin4en1  9169  isfin4-3  9175  isfin32i  9225  fin45  9252  fin56  9253  fin67  9255  hsmexlem1  9286  hsmexlem3  9288  axcc3  9298  ttukeylem1  9369  brdom3  9388  iundom2g  9400  iundom  9402  iunctb  9434  gchi  9484  engch  9488  gchdomtri  9489  fpwwe2lem6  9495  fpwwe2lem7  9496  fpwwe2lem9  9498  gchpwdom  9530  prcdnq  9853  reexALT  11864  hasheni  13176  hashdomi  13207  brfi1indALT  13320  climcl  14274  climi  14285  climrlim2  14322  climrecl  14358  climge0  14359  iseralt  14459  climfsum  14596  structex  15915  issubc  16542  pmtrfv  17918  dprdval  18448  frgpcyg  19970  lindff  20202  lindfind  20203  f1lindf  20209  lindfmm  20214  lsslindf  20217  lbslcic  20228  1stcrestlem  21303  2ndcdisj2  21308  dis2ndc  21311  hauspwdom  21352  refbas  21361  refssex  21362  reftr  21365  refun0  21366  ovoliunnul  23321  uniiccdif  23392  dvle  23815  subgrv  26207  cyclnspth  26751  hlimi  28173  brsset  32121  brbigcup  32130  elfix2  32136  brcolinear2  32290  isfne  32459  refssfne  32478  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  brabg2  33640  heiborlem4  33743  isrngo  33826  isdivrngo  33879  brssr  34391  fphpd  37697  ctbnfien  37699  climd  40222  climuzlem  40293  rlimdmafv  41578  linindsv  42559