Theorem psseq2 4044

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 3962	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
2		neeq2 3019	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
3	1, 2	anbi12d 641	. 2 ⊢ (𝐴 = 𝐵 → ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴) ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵)))
4		df-pss 3924	. 2 ⊢ (𝐶 ⊊ 𝐴 ↔ (𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴))
5		df-pss 3924	. 2 ⊢ (𝐶 ⊊ 𝐵 ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵))
6	3, 4, 5	3bitr4g 316	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ≠ wne 2956   ⊆ wss 3904   ⊊ wpss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ne 2957  df-ss 3921  df-pss 3924

This theorem is referenced by:  psseq2i  4046  psseq2d  4049  psssstr  4063  brrpssg  7704  sorpssint  7712  pssnn  9133  php  9171  isfin4  10251  fin2i2  10272  elnp  10942  elnpi  10943  ltprord  10985  pgpfac1lem1  20099  pgpfac1lem5  20104  lbsextlem4  21211  alexsubALTlem4  24090  spansncv  31802  cvbr  32431  cvcon3  32433  cvnbtwn  32435  cvbr4i  32516  ssdifidlprm  33606  ssmxidl  33623  dfon2lem6  36100  dfon2lem7  36101  dfon2lem8  36102  dfon2  36104  lcvbr  39609  lcvnbtwn  39613  lsatcv0  39619  lsat0cv  39621  islshpcv  39641  mapdcv  42248  pssn0  42810  nthrucw  47426