Theorem psseq2 4047

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 3965	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
2		neeq2 3023	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
3	1, 2	anbi12d 643	. 2 ⊢ (𝐴 = 𝐵 → ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴) ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵)))
4		df-pss 3927	. 2 ⊢ (𝐶 ⊊ 𝐴 ↔ (𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴))
5		df-pss 3927	. 2 ⊢ (𝐶 ⊊ 𝐵 ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1563   ≠ wne 2960   ⊆ wss 3907   ⊊ wpss 3908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ne 2961  df-ss 3924  df-pss 3927

This theorem is referenced by:  psseq2i  4049  psseq2d  4052  psssstr  4066  brrpssg  7712  sorpssint  7720  pssnn  9141  php  9179  isfin4  10269  fin2i2  10290  elnp  10960  elnpi  10961  ltprord  11003  pgpfac1lem1  20137  pgpfac1lem5  20142  lbsextlem4  21254  ssdifidlprm  21446  alexsubALTlem4  24168  spansncv  31914  cvbr  32543  cvcon3  32545  cvnbtwn  32547  cvbr4i  32628  ssmxidl  33674  dfon2lem6  36149  dfon2lem7  36150  dfon2lem8  36151  dfon2  36153  lcvbr  39657  lcvnbtwn  39661  lsatcv0  39667  lsat0cv  39669  islshpcv  39689  mapdcv  42296  pssn0  42858  nthrucw  47460