Theorem prid1 3689

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 3687	. 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ {𝐴, 𝐵})
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ {𝐴, 𝐵}

Syntax hints:   ∈ wcel 2141  Vcvv 2730  {cpr 3584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590

This theorem is referenced by:  prid2  3690  prnz  3705  preqr1  3755  preq12b  3757  prel12  3758  opi1  4217  opeluu  4435  onsucelsucexmidlem1  4512  regexmidlem1  4517  reg2exmidlema  4518  opthreg  4540  ordtri2or2exmid  4555  ontri2orexmidim  4556  dmrnssfld  4874  funopg  5232  acexmidlemb  5845  0lt2o  6420  2dom  6783  unfiexmid  6895  djuss  7047  exmidomni  7118  exmidonfinlem  7170  exmidaclem  7185  reelprrecn  7909  pnfxr  7972  sup3exmid  8873  lgsdir2lem3  13725  bdop  13910  2o01f  14029  iswomni0  14083