MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  brrelexi Structured version   Visualization version   GIF version

Theorem brrelexi 5355
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
StepHypRef Expression
1 brrelexi.1 . 2 Rel 𝑅
2 brrelex 5353 . 2 ((Rel 𝑅𝐴𝑅𝐵) → 𝐴 ∈ V)
31, 2mpan 673 1 (𝐴𝑅𝐵𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2158  Vcvv 3390   class class class wbr 4840  Rel wrel 5313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-sep 4971  ax-nul 4980  ax-pr 5093
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ral 3100  df-rex 3101  df-rab 3104  df-v 3392  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-nul 4114  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-br 4841  df-opab 4903  df-xp 5314  df-rel 5315
This theorem is referenced by:  nprrel  5358  vtoclr  5361  opeliunxp2  5459  ideqg  5472  issetid  5475  dffv2  6489  brfvopabrbr  6497  brrpssg  7166  opeliunxp2f  7568  brtpos2  7590  brdomg  8199  isfi  8213  en1uniel  8261  domdifsn  8279  undom  8284  xpdom2  8291  xpdom1g  8293  sbth  8316  dom0  8324  sdom0  8328  sdomirr  8333  sdomdif  8344  fodomr  8347  pwdom  8348  xpen  8359  pwen  8369  php3  8382  sucdom2  8392  sdom1  8396  fineqv  8411  f1finf1o  8423  infsdomnn  8457  relprcnfsupp  8514  fsuppimp  8517  fsuppunbi  8532  mapfien2  8550  harword  8706  brwdom  8708  domwdom  8715  brwdom3i  8724  unwdomg  8725  xpwdomg  8726  infdifsn  8798  ac10ct  9137  inffien  9166  iunfictbso  9217  cdaen  9277  cdadom1  9290  cdafi  9294  cdainflem  9295  cdalepw  9300  unctb  9309  infcdaabs  9310  infunabs  9311  infmap2  9322  cfslb2n  9372  fin4i  9402  isfin5  9403  isfin6  9404  fin4en1  9413  isfin4-3  9419  isfin32i  9469  fin45  9496  fin56  9497  fin67  9499  hsmexlem1  9530  hsmexlem3  9532  axcc3  9542  ttukeylem1  9613  brdom3  9632  iundom2g  9644  iundom  9646  iunctb  9678  gchi  9728  engch  9732  gchdomtri  9733  fpwwe2lem6  9739  fpwwe2lem7  9740  fpwwe2lem9  9742  gchpwdom  9774  prcdnq  10097  reexALT  12036  hasheni  13352  hashdomi  13383  brfi1indALT  13495  climcl  14449  climi  14460  climrlim2  14497  climrecl  14533  climge0  14534  iseralt  14634  climfsum  14770  structex  16075  issubc  16695  pmtrfv  18069  dprdval  18600  frgpcyg  20125  lindff  20360  lindfind  20361  f1lindf  20367  lindfmm  20372  lsslindf  20375  lbslcic  20386  1stcrestlem  21465  2ndcdisj2  21470  dis2ndc  21473  hauspwdom  21514  refbas  21523  refssex  21524  reftr  21527  refun0  21528  ovoliunnul  23484  uniiccdif  23555  dvle  23980  subgrv  26374  cyclnspth  26920  hlimi  28370  brsset  32314  brbigcup  32323  elfix2  32329  brcolinear2  32483  isfne  32652  refssfne  32671  ovoliunnfl  33761  voliunnfl  33763  volsupnfl  33764  brabg2  33819  heiborlem4  33921  isrngo  34004  isdivrngo  34057  brssr  34561  fphpd  37879  ctbnfien  37881  climd  40381  climuzlem  40452  rlimdmafv  41763  rlimdmafv2  41844  linindsv  42799
  Copyright terms: Public domain W3C validator