MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  psseq1 Structured version   Unicode version

Theorem psseq1 3532
Description: Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.)
Assertion
Ref Expression
psseq1  |-  ( A  =  B  ->  ( A  C.  C  <->  B  C.  C
) )

Proof of Theorem psseq1
StepHypRef Expression
1 sseq1 3465 . . 3  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
2 neeq1 2686 . . 3  |-  ( A  =  B  ->  ( A  =/=  C  <->  B  =/=  C ) )
31, 2anbi12d 711 . 2  |-  ( A  =  B  ->  (
( A  C_  C  /\  A  =/=  C
)  <->  ( B  C_  C  /\  B  =/=  C
) ) )
4 df-pss 3432 . 2  |-  ( A 
C.  C  <->  ( A  C_  C  /\  A  =/= 
C ) )
5 df-pss 3432 . 2  |-  ( B 
C.  C  <->  ( B  C_  C  /\  B  =/= 
C ) )
63, 4, 53bitr4g 290 1  |-  ( A  =  B  ->  ( A  C.  C  <->  B  C.  C
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 186    /\ wa 369    = wceq 1407    =/= wne 2600    C_ wss 3416    C. wpss 3417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-ne 2602  df-in 3423  df-ss 3430  df-pss 3432
This theorem is referenced by:  psseq1i  3534  psseq1d  3537  psstr  3549  sspsstr  3550  brrpssg  6566  sorpssuni  6573  pssnn  7775  marypha1lem  7929  infeq5i  8088  infpss  8631  fin4i  8712  isfin2-2  8733  zornn0g  8919  ttukeylem7  8929  elnp  9397  elnpi  9398  ltprord  9440  pgpfac1lem1  17447  pgpfac1lem5  17452  pgpfac1  17453  pgpfaclem2  17455  pgpfac  17457  islbs3  18123  alexsubALTlem4  20844  wilthlem2  23726  spansncv  26998  cvbr  27627  cvcon3  27629  cvnbtwn  27631  dfon2lem3  30017  dfon2lem4  30018  dfon2lem5  30019  dfon2lem6  30020  dfon2lem7  30021  dfon2lem8  30022  dfon2  30024  lcvbr  32052  lcvnbtwn  32056  mapdcv  34693
  Copyright terms: Public domain W3C validator