Theorem psseq2 4086

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534   ≠ wne 2937   ⊆ wss 3947   ⊊ wpss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-v 3473  df-in 3954  df-ss 3964  df-pss 3966

This theorem is referenced by:  psseq2i  4088  psseq2d  4091  psssstr  4104  brrpssg  7730  sorpssint  7738  pssnn  9193  php  9235  phpOLD  9247  php2OLD  9248  pssnnOLD  9290  isfin4  10321  fin2i2  10342  elnp  11011  elnpi  11012  ltprord  11054  pgpfac1lem1  20031  pgpfac1lem5  20036  lbsextlem4  21049  alexsubALTlem4  23967  spansncv  31476  cvbr  32105  cvcon3  32107  cvnbtwn  32109  cvbr4i  32190  ssmxidl  33200  dfon2lem6  35384  dfon2lem7  35385  dfon2lem8  35386  dfon2  35388  lcvbr  38493  lcvnbtwn  38497  lsatcv0  38503  lsat0cv  38505  islshpcv  38525  mapdcv  41133  pssn0  41715