Theorem prid1g 4742

Description: An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)

Assertion

Ref	Expression
prid1g	⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})

Proof of Theorem prid1g

Step	Hyp	Ref	Expression
1		eqid 2734	. . 3 ⊢ 𝐴 = 𝐴
2	1	orci 865	. 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)
3		elprg 4630	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)))
4	2, 3	mpbiri 258	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1539   ∈ wcel 2107  {cpr 4610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3466  df-un 3938  df-sn 4609  df-pr 4611

This theorem is referenced by:  prid2g  4743  prid1  4744  prnzg  4760  preq1b  4828  prel12g  4846  elpreqprb  4850  prproe  4887  opth1  5462  fr2nr  5644  fpr2g  7214  f1prex  7287  fveqf1o  7305  fvf1pr  7310  pw2f1olem  9099  hashprdifel  14420  gcdcllem3  16521  mgm2nsgrplem1  18905  mgm2nsgrplem2  18906  mgm2nsgrplem3  18907  sgrp2nmndlem1  18910  sgrp2rid2  18913  pmtrprfv  19444  pptbas  22981  coseq0negpitopi  26500  uhgr2edg  29172  umgrvad2edg  29177  uspgr2v1e2w  29215  usgr2v1e2w  29216  nbusgredgeu0  29332  nbusgrf1o0  29333  nb3grprlem1  29344  nb3grprlem2  29345  vtxduhgr0nedg  29457  1hegrvtxdg1  29472  1egrvtxdg1  29474  umgr2v2evd2  29492  vdegp1bi  29502  mptprop  32654  altgnsg  33115  cyc3genpmlem  33117  elrspunsn  33398  bj-prmoore  37057  ftc1anclem8  37648  kelac2  43022  pr2el1  43507  pr2eldif1  43512  fourierdlem54  46120  sge0pr  46354  imarnf1pr  47240  paireqne  47444  fmtnoprmfac2lem1  47499  1hegrlfgr  47994  termc2  49117