Theorem prid1 3799

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

Syntax hints:   ∈ wcel 2205  Vcvv 2815  {cpr 3692

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3217  df-sn 3697  df-pr 3698

This theorem is referenced by:  prid2  3800  prnz  3817  preqr1  3874  preq12b  3876  prel12  3877  opi1  4350  opeluu  4573  onsucelsucexmidlem1  4652  regexmidlem1  4657  reg2exmidlema  4658  opthreg  4680  ordtri2or2exmid  4695  ontri2orexmidim  4696  dmrnssfld  5022  funopg  5388  acexmidlemb  6044  0lt2o  6676  2dom  7048  unfiexmid  7180  djuss  7363  exmidomni  7435  pr2cv1  7494  exmidonfinlem  7498  exmidaclem  7517  reelprrecn  8264  pnfxr  8328  sup3exmid  9233  fun2dmnop0  11226  fnpr2ob  13570  lgsdir2lem3  15920  upgrex  16115  upgr1een  16136  eulerpathprum  16492  bdop  16662  2o01f  16785  iswomni0  16853