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

Theorem prid1 4404
Description: An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 24-Jun-1993.)
Hypothesis
Ref Expression
prid1.1 𝐴 ∈ V
Assertion
Ref Expression
prid1 𝐴 ∈ {𝐴, 𝐵}

Proof of Theorem prid1
StepHypRef Expression
1 prid1.1 . 2 𝐴 ∈ V
2 prid1g 4402 . 2 (𝐴 ∈ V → 𝐴 ∈ {𝐴, 𝐵})
31, 2ax-mp 5 1 𝐴 ∈ {𝐴, 𝐵}
Colors of variables: wff setvar class
Syntax hints:  wcel 2103  Vcvv 3304  {cpr 4287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-v 3306  df-un 3685  df-sn 4286  df-pr 4288
This theorem is referenced by:  prid2  4405  prnz  4416  preq12b  4489  prel12  4490  unisn2  4902  opi1  5041  opeluu  5043  dmrnssfld  5491  funopg  6035  fveqf1o  6672  2dom  8145  opthreg  8628  dfac2  9066  brdom7disj  9466  brdom6disj  9467  reelprrecn  10141  pnfxr  10205  m1expcl2  12997  hash2prb  13367  sadcf  15298  prmreclem2  15744  xpsfrnel2  16348  setcepi  16860  grpss  17562  efgi0  18254  vrgpf  18302  vrgpinv  18303  frgpuptinv  18305  frgpup2  18310  frgpnabllem1  18397  dmdprdpr  18569  dprdpr  18570  cnmsgnsubg  20046  m2detleiblem5  20554  m2detleiblem3  20558  m2detleiblem4  20559  m2detleib  20560  indistopon  20928  indiscld  21018  xpstopnlem1  21735  xpstopnlem2  21737  xpsdsval  22308  i1f1lem  23576  i1f1  23577  dvnfre  23835  c1lip2  23881  aannenlem2  24204  cxplogb  24644  ppiublem2  25048  lgsdir2lem3  25172  eengbas  25981  ebtwntg  25982  structvtxval  26030  usgr2trlncl  26787  umgrwwlks2on  26999  wlk2v2e  27230  eulerpathpr  27313  psgnid  30077  prsiga  30424  coinflippvt  30776  subfacp1lem3  31392  kur14lem7  31422  fprb  31897  noxp1o  32043  noextendlt  32049  nosepdmlem  32060  nolt02o  32072  nosupbnd1lem5  32085  nosupbnd2lem1  32088  noetalem1  32090  onint1  32675  poimirlem22  33663  pw2f1ocnv  38023  fvrcllb0d  38404  fvrcllb0da  38405  corclrcl  38418  relexp0idm  38426  corcltrcl  38450  refsum2cnlem1  39612  limsup10exlem  40424  fourierdlem103  40846  fourierdlem104  40847  prsal  40958  zlmodzxzscm  42562  zlmodzxzldeplem3  42718
  Copyright terms: Public domain W3C validator