Theorem psseq2 4042

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ≠ wne 2957   ⊆ wss 3902   ⊊ wpss 3903

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ne 2958  df-ss 3919  df-pss 3922

This theorem is used by:  psseq2i  4044  psseq2d  4047  psssstr  4061  brrpssg  7730  sorpssint  7738  pssnn  9167  php  9205  isfin4  10303  fin2i2  10324  elnp  11000  elnpi  11001  ltprord  11043  pgpfac1lem1  20209  pgpfac1lem5  20214  lbsextlem4  21354  ssdifidlprm  21555  alexsubALTlem4  24282  spansncv  32142  cvbr  32771  cvcon3  32773  cvnbtwn  32775  cvbr4i  32856  ssmxidl  33885  dfon2lem6  36373  dfon2lem7  36374  dfon2lem8  36375  dfon2  36377  findcard4  38471  lcvbr  39902  lcvnbtwn  39906  lsatcv0  39912  lsat0cv  39914  islshpcv  39934  mapdcv  42541  pssn0  43105