ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elpri GIF version

Theorem elpri 3554
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 3551 . 2 (𝐴 ∈ {𝐵, 𝐶} → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
21ibi 175 1 (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵𝐴 = 𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wo 698   = wceq 1332  wcel 1481  {cpr 3532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3079  df-sn 3537  df-pr 3538
This theorem is referenced by:  nelpri  3555  nelprd  3557  opth1  4165  0nelop  4177  ontr2exmid  4447  onintexmid  4494  reg3exmidlemwe  4500  funtpg  5181  ftpg  5611  acexmidlemcase  5776  2oconcl  6343  en2eqpr  6808  eldju1st  6963  finomni  7019  exmidomniim  7020  ismkvnex  7036  exmidonfinlem  7065  exmidfodomrlemr  7074  exmidfodomrlemrALT  7075  exmidaclem  7080  sup3exmid  8738  m1expcl2  10345  maxleim  11008  maxleast  11016  zmaxcl  11027  minmax  11032  xrmaxleim  11044  xrmaxaddlem  11060  xrminmax  11065  unct  11989  qtopbas  12728  limcimolemlt  12839  recnprss  12862  coseq0negpitopi  12963  el2oss1o  13357  012of  13361  2o01f  13362  nninfalllem1  13376  nninfall  13377  nninfsellemqall  13384  nninfomnilem  13387  trilpolemclim  13402  trilpolemcl  13403  trilpolemisumle  13404  trilpolemeq1  13406  trilpolemlt1  13407
  Copyright terms: Public domain W3C validator