Theorem brrelexi 5158

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

Syntax hints:   → wi 4   ∈ wcel 1990  Vcvv 3200   class class class wbr 4653  Rel wrel 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-rel 5121

This theorem is referenced by:  nprrel  5161  vtoclr  5164  opeliunxp2  5260  ideqg  5273  issetid  5276  dffv2  6271  brfvopabrbr  6279  brrpssg  6939  opeliunxp2f  7336  brtpos2  7358  brdomg  7965  isfi  7979  en1uniel  8028  domdifsn  8043  undom  8048  xpdom2  8055  xpdom1g  8057  sbth  8080  dom0  8088  sdom0  8092  sdomirr  8097  sdomdif  8108  fodomr  8111  pwdom  8112  xpen  8123  pwen  8133  php3  8146  sucdom2  8156  sdom1  8160  fineqv  8175  f1finf1o  8187  infsdomnn  8221  relprcnfsupp  8278  fsuppimp  8281  fsuppunbi  8296  mapfien2  8314  harword  8470  brwdom  8472  domwdom  8479  brwdom3i  8488  unwdomg  8489  xpwdomg  8490  infdifsn  8554  ac10ct  8857  inffien  8886  iunfictbso  8937  cdaen  8995  cdadom1  9008  cdafi  9012  cdainflem  9013  cdalepw  9018  unctb  9027  infcdaabs  9028  infunabs  9029  infmap2  9040  cfslb2n  9090  fin4i  9120  isfin5  9121  isfin6  9122  fin4en1  9131  isfin4-3  9137  isfin32i  9187  fin45  9214  fin56  9215  fin67  9217  hsmexlem1  9248  hsmexlem3  9250  axcc3  9260  ttukeylem1  9331  brdom3  9350  iundom2g  9362  iundom  9364  iunctb  9396  gchi  9446  engch  9450  gchdomtri  9451  fpwwe2lem6  9457  fpwwe2lem7  9458  fpwwe2lem9  9460  gchpwdom  9492  prcdnq  9815  reexALT  11826  hasheni  13136  hashdomi  13169  brfi1indALT  13282  brfi1indALTOLD  13288  climcl  14230  climi  14241  climrlim2  14278  climrecl  14314  climge0  14315  iseralt  14415  climfsum  14552  structex  15868  issubc  16495  pmtrfv  17872  dprdval  18402  frgpcyg  19922  lindff  20154  lindfind  20155  f1lindf  20161  lindfmm  20166  lsslindf  20169  lbslcic  20180  1stcrestlem  21255  2ndcdisj2  21260  dis2ndc  21263  hauspwdom  21304  refbas  21313  refssex  21314  reftr  21317  refun0  21318  ovoliunnul  23275  uniiccdif  23346  dvle  23770  subgrv  26162  cyclnspth  26695  hlimi  28045  brsset  31996  brbigcup  32005  elfix2  32011  brcolinear2  32165  isfne  32334  refssfne  32353  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  brabg2  33510  heiborlem4  33613  isrngo  33696  isdivrngo  33749  fphpd  37380  ctbnfien  37382  climd  39904  climuzlem  39975  rlimdmafv  41257  linindsv  42234