Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elpri Structured version   Visualization version   GIF version

Theorem elpri 4188
 Description: If a class is an element of a pair, then it is one of the two paired elements. (Contributed by Scott Fenton, 1-Apr-2011.)
Assertion
Ref Expression
elpri (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵𝐴 = 𝐶))

Proof of Theorem elpri
StepHypRef Expression
1 elprg 4187 . 2 (𝐴 ∈ {𝐵, 𝐶} → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
21ibi 256 1 (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵𝐴 = 𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 383   = wceq 1481   ∈ wcel 1988  {cpr 4170 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-un 3572  df-sn 4169  df-pr 4171 This theorem is referenced by:  elpr2OLD  4191  nelpri  4192  nelprd  4194  tppreqb  4327  elpreqpr  4387  elpr2elpr  4389  prproe  4425  3elpr2eq  4426  opth1  4934  0nelop  4950  funtpgOLD  5931  ftpg  6408  2oconcl  7568  cantnflem2  8572  m1expcl2  12865  hash2pwpr  13241  bitsinv1lem  15144  prm23lt5  15500  xpscfv  16203  xpsfeq  16205  pmtrprfval  17888  m1expaddsub  17899  psgnprfval  17922  frgpuptinv  18165  frgpup3lem  18171  cnmsgnsubg  19904  zrhpsgnelbas  19921  mdetralt  20395  m2detleiblem1  20411  indiscld  20876  cnindis  21077  connclo  21199  txindis  21418  xpsxmetlem  22165  xpsmet  22168  ishl2  23147  recnprss  23649  recnperf  23650  dvlip2  23739  coseq0negpitopi  24236  pythag  24528  reasinsin  24604  scvxcvx  24693  perfectlem2  24936  lgslem4  25006  lgseisenlem2  25082  2lgsoddprmlem3  25120  usgredg4  26090  konigsberg  27099  ex-pr  27257  elpreq  29332  1neg1t1neg1  29488  signswch  30612  kur14lem7  31168  poimirlem31  33411  ftc1anclem2  33457  wepwsolem  37431  relexp01min  37824  clsk1indlem1  38163  ssrecnpr  38327  seff  38328  sblpnf  38329  expgrowthi  38352  dvconstbi  38353  sumpair  39014  refsum2cnlem1  39016  iooinlbub  39526  elprn1  39665  elprn2  39666  cncfiooicclem1  39869  dvmptconst  39892  dvmptidg  39894  dvmulcncf  39903  dvdivcncf  39905  elprneb  41059  perfectALTVlem2  41396  0dig2pr01  42169
 Copyright terms: Public domain W3C validator