Theorem psseq2 3948

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

Assertion

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

Proof of Theorem psseq2

Step	Hyp	Ref	Expression
1		sseq2 3876	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
2		neeq2 3023	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
3	1, 2	anbi12d 622	. 2 ⊢ (𝐴 = 𝐵 → ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴) ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵)))
4		df-pss 3838	. 2 ⊢ (𝐶 ⊊ 𝐴 ↔ (𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴))
5		df-pss 3838	. 2 ⊢ (𝐶 ⊊ 𝐵 ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵))
6	3, 4, 5	3bitr4g 306	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1508   ≠ wne 2960   ⊆ wss 3822   ⊊ wpss 3823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2743

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2752  df-cleq 2764  df-clel 2839  df-ne 2961  df-in 3829  df-ss 3836  df-pss 3838

This theorem is referenced by:  psseq2i  3950  psseq2d  3953  psssstr  3966  brrpssg  7267  sorpssint  7275  php  8495  php2  8496  pssnn  8529  isfin4  9515  fin2i2  9536  elnp  10205  elnpi  10206  ltprord  10248  pgpfac1lem1  18958  pgpfac1lem5  18963  lbsextlem4  19667  alexsubALTlem4  22377  spansncv  29226  cvbr  29855  cvcon3  29857  cvnbtwn  29859  cvbr4i  29940  dfon2lem6  32590  dfon2lem7  32591  dfon2lem8  32592  dfon2  32594  lcvbr  35639  lcvnbtwn  35643  lsatcv0  35649  lsat0cv  35651  islshpcv  35671  mapdcv  38278  pssn0  38596