Theorem prid1 3775

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

Syntax hints:   ∈ wcel 2200  Vcvv 2800  {cpr 3668

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674

This theorem is referenced by:  prid2  3776  prnz  3793  preqr1  3849  preq12b  3851  prel12  3852  opi1  4322  opeluu  4545  onsucelsucexmidlem1  4624  regexmidlem1  4629  reg2exmidlema  4630  opthreg  4652  ordtri2or2exmid  4667  ontri2orexmidim  4668  dmrnssfld  4993  funopg  5358  acexmidlemb  6005  0lt2o  6604  2dom  6975  unfiexmid  7103  djuss  7260  exmidomni  7332  pr2cv1  7391  exmidonfinlem  7394  exmidaclem  7413  reelprrecn  8157  pnfxr  8222  sup3exmid  9127  fun2dmnop0  11101  fnpr2ob  13413  lgsdir2lem3  15749  upgrex  15944  bdop  16406  2o01f  16529  iswomni0  16591