Theorem psseq1 4067

Description: Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.)

Assertion

Ref	Expression
psseq1	⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶))

Proof of Theorem psseq1

Step	Hyp	Ref	Expression
1		sseq1 3995	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
2		neeq1 3081	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶)))
4		df-pss 3957	. 2 ⊢ (𝐴 ⊊ 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶))
5		df-pss 3957	. 2 ⊢ (𝐵 ⊊ 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶))
6	3, 4, 5	3bitr4g 316	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1536   ≠ wne 3019   ⊆ wss 3939   ⊊ wpss 3940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-ne 3020  df-in 3946  df-ss 3955  df-pss 3957

This theorem is referenced by:  psseq1i  4069  psseq1d  4072  psstr  4084  sspsstr  4085  brrpssg  7454  sorpssuni  7461  pssnn  8739  marypha1lem  8900  infeq5i  9102  infpss  9642  fin4i  9723  isfin2-2  9744  zornn0g  9930  ttukeylem7  9940  elnp  10412  elnpi  10413  ltprord  10455  pgpfac1lem1  19199  pgpfac1lem5  19204  pgpfac1  19205  pgpfaclem2  19207  pgpfac  19209  islbs3  19930  alexsubALTlem4  22661  wilthlem2  25649  spansncv  29433  cvbr  30062  cvcon3  30064  cvnbtwn  30066  dfon2lem3  33034  dfon2lem4  33035  dfon2lem5  33036  dfon2lem6  33037  dfon2lem7  33038  dfon2lem8  33039  dfon2  33041  lcvbr  36161  lcvnbtwn  36165  mapdcv  38800