Theorem psseq2 4087

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 4007	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
2		neeq2 3004	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
3	1, 2	anbi12d 631	. 2 ⊢ (𝐴 = 𝐵 → ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴) ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵)))
4		df-pss 3966	. 2 ⊢ (𝐶 ⊊ 𝐴 ↔ (𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴))
5		df-pss 3966	. 2 ⊢ (𝐶 ⊊ 𝐵 ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵))
6	3, 4, 5	3bitr4g 313	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ≠ wne 2940   ⊆ wss 3947   ⊊ wpss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-v 3476  df-in 3954  df-ss 3964  df-pss 3966

This theorem is referenced by:  psseq2i  4089  psseq2d  4092  psssstr  4105  brrpssg  7711  sorpssint  7719  pssnn  9164  php  9206  phpOLD  9218  php2OLD  9219  pssnnOLD  9261  isfin4  10288  fin2i2  10309  elnp  10978  elnpi  10979  ltprord  11021  pgpfac1lem1  19938  pgpfac1lem5  19943  lbsextlem4  20766  alexsubALTlem4  23545  spansncv  30893  cvbr  31522  cvcon3  31524  cvnbtwn  31526  cvbr4i  31607  ssmxidl  32578  dfon2lem6  34748  dfon2lem7  34749  dfon2lem8  34750  dfon2  34752  lcvbr  37879  lcvnbtwn  37883  lsatcv0  37889  lsat0cv  37891  islshpcv  37911  mapdcv  40519  pssn0  41041