Theorem prid1g 4720

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 2760	. . 3 ⊢ 𝐴 = 𝐴
2	1	orci 879	. 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)
3		elprg 4606	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)))
4	2, 3	mpbiri 261	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1569   ∈ wcel 2144  {cpr 4585

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151  df-sn 4584  df-pr 4586

This theorem is used by:  prid2g  4721  prid1  4722  prnzg  4738  preq1b  4805  prel12g  4823  elpreqprb  4827  prproe  4864  opth1  5443  fr2nr  5627  fpr2g  7217  f1prex  7292  fveqf1o  7310  fvf1pr  7315  pw2f1olem  9100  hashprdifel  14542  gcdcllem3  16671  mgm2nsgrplem1  19117  mgm2nsgrplem2  19118  mgm2nsgrplem3  19119  sgrp2nmndlem1  19122  sgrp2rid2  19125  pmtrprfv  19667  pptbas  23326  coseq0negpitopi  26832  uhgr2edg  29789  umgrvad2edg  29794  uspgr2v1e2w  29832  usgr2v1e2w  29833  nbusgredgeu0  29949  nbusgrf1o0  29950  nb3grprlem1  29961  nb3grprlem2  29962  vtxduhgr0nedg  30073  1hegrvtxdg1  30088  1egrvtxdg1  30090  umgr2v2evd2  30108  vdegp1bi  30118  mptprop  33291  altgnsg  33710  cyc3genpmlem  33712  elrspunsn  33979  esplyfval1  34205  bj-prmoore  38036  ftc1anclem8  38619  kelac2  44067  pr2el1  44550  pr2eldif1  44555  fourierdlem54  47170  sge0pr  47404  imarnf1pr  48352  paireqne  48593  fmtnoprmfac2lem1  48651  grlimprclnbgr  49094  grlimprclnbgredg  49095  1hegrlfgr  49230  fucoppcffth  50519  termc2  50626  uobeqterm  50654  2arwcatlem4  50706  incat  50709