Theorem prid1 3710

Description: An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-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 3708	. 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ {𝐴, 𝐵})
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ {𝐴, 𝐵}

Syntax hints:   ∈ wcel 2158  Vcvv 2749  {cpr 3605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-v 2751  df-un 3145  df-sn 3610  df-pr 3611

This theorem is referenced by:  prid2  3711  prnz  3726  preqr1  3780  preq12b  3782  prel12  3783  opi1  4244  opeluu  4462  onsucelsucexmidlem1  4539  regexmidlem1  4544  reg2exmidlema  4545  opthreg  4567  ordtri2or2exmid  4582  ontri2orexmidim  4583  dmrnssfld  4902  funopg  5262  acexmidlemb  5880  0lt2o  6456  2dom  6819  unfiexmid  6931  djuss  7083  exmidomni  7154  exmidonfinlem  7206  exmidaclem  7221  reelprrecn  7960  pnfxr  8024  sup3exmid  8928  fnpr2ob  12778  lgsdir2lem3  14784  bdop  14980  2o01f  15100  iswomni0  15153