Theorem prid1 3698

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

Syntax hints:   ∈ wcel 2148  Vcvv 2737  {cpr 3593

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599

This theorem is referenced by:  prid2  3699  prnz  3714  preqr1  3767  preq12b  3769  prel12  3770  opi1  4230  opeluu  4448  onsucelsucexmidlem1  4525  regexmidlem1  4530  reg2exmidlema  4531  opthreg  4553  ordtri2or2exmid  4568  ontri2orexmidim  4569  dmrnssfld  4887  funopg  5247  acexmidlemb  5862  0lt2o  6437  2dom  6800  unfiexmid  6912  djuss  7064  exmidomni  7135  exmidonfinlem  7187  exmidaclem  7202  reelprrecn  7941  pnfxr  8004  sup3exmid  8908  lgsdir2lem3  14213  bdop  14398  2o01f  14517  iswomni0  14570