Theorem prid1 3744

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

Syntax hints:   ∈ wcel 2177  Vcvv 2773  {cpr 3639

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645

This theorem is referenced by:  prid2  3745  prnz  3761  preqr1  3815  preq12b  3817  prel12  3818  opi1  4284  opeluu  4505  onsucelsucexmidlem1  4584  regexmidlem1  4589  reg2exmidlema  4590  opthreg  4612  ordtri2or2exmid  4627  ontri2orexmidim  4628  dmrnssfld  4950  funopg  5314  acexmidlemb  5949  0lt2o  6540  2dom  6911  unfiexmid  7030  djuss  7187  exmidomni  7259  exmidonfinlem  7317  exmidaclem  7336  reelprrecn  8080  pnfxr  8145  sup3exmid  9050  fun2dmnop0  11014  fnpr2ob  13247  lgsdir2lem3  15582  upgrex  15774  bdop  15949  2o01f  16070  iswomni0  16131