Theorem prid1 4700

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

Step	Hyp	Ref	Expression
1		prid1.1	. 2 ⊢ 𝐴 ∈ V
2		prid1g 4698	. 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ {𝐴, 𝐵})
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ {𝐴, 𝐵}

Syntax hints:   ∈ wcel 2114  Vcvv 3496  {cpr 4571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943  df-sn 4570  df-pr 4572

This theorem is referenced by:  prid2  4701  prnz  4714  preq12b  4783  unisn2  5218  opi1  5362  opeluu  5364  dmrnssfld  5843  funopg  6391  fprb  6958  fveqf1o  7060  2dom  8584  opthreg  9083  djuss  9351  dfac2b  9558  brdom7disj  9955  brdom6disj  9956  reelprrecn  10631  pnfxr  10697  m1expcl2  13454  hash2prb  13833  sadcf  15804  prmreclem2  16255  fnpr2ob  16833  setcepi  17350  grpss  18123  efgi0  18848  vrgpf  18896  vrgpinv  18897  frgpuptinv  18899  frgpup2  18904  frgpnabllem1  18995  dmdprdpr  19173  dprdpr  19174  cnmsgnsubg  20723  m2detleiblem5  21236  m2detleiblem3  21240  m2detleiblem4  21241  m2detleib  21242  indistopon  21611  indiscld  21701  xpstopnlem1  22419  xpstopnlem2  22421  xpsdsval  22993  ehl2eudis  24027  i1f1lem  24292  i1f1  24293  dvnfre  24551  c1lip2  24597  aannenlem2  24920  cxplogb  25366  ppiublem2  25781  lgsdir2lem3  25905  eengbas  26769  ebtwntg  26770  structvtxval  26808  usgr2trlncl  27543  umgrwwlks2on  27738  wlk2v2e  27938  eulerpathpr  28021  s2rn  30622  psgnid  30741  trsp2cyc  30767  cyc3fv1  30781  cnmsgn0g  30790  prsiga  31392  coinflippvt  31744  subfacp1lem3  32431  kur14lem7  32461  ex-sategoelel12  32676  noxp1o  33172  noextendlt  33178  nosepdmlem  33189  nolt02o  33201  nosupbnd1lem5  33214  nosupbnd2lem1  33217  noetalem1  33219  onint1  33799  poimirlem22  34916  pw2f1ocnv  39641  fvrcllb0d  40045  fvrcllb0da  40046  corclrcl  40059  relexp0idm  40067  corcltrcl  40091  mnuprdlem1  40615  mnuprdlem3  40617  mnurndlem1  40624  refsum2cnlem1  41301  limsup10exlem  42060  fourierdlem103  42501  fourierdlem104  42502  prsal  42610  zlmodzxzscm  44412  zlmodzxzldeplem3  44564  rrx2pxel  44705  rrx2linesl  44737  2sphere0  44744