Theorem dfpss2 4039

Description: Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.)

Assertion

Ref	Expression
dfpss2	⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))

Proof of Theorem dfpss2

Step	Hyp	Ref	Expression
1		df-pss 3923	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2		df-ne 2926	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	anbi2i 623	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
4	1, 3	bitri 275	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1540   ≠ wne 2925   ⊆ wss 3903   ⊊ wpss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-ne 2926  df-pss 3923

This theorem is referenced by:  dfpss3  4040  sspss  4053  psstr  4058  npss  4064  ssnelpss  4065  pssv  4400  disj4  4410  f1imapss  7203  pssnn  9082  phpeqd  9126  nnsdomo  9132  inf3lem6  9529  ssfin4  10204  fin23lem25  10218  fin23lem38  10243  isf32lem2  10248  pwfseqlem4  10556  genpcl  10902  prlem934  10927  ltaddpr  10928  sltlpss  27822  chnlei  31429  cvbr2  32227  cvnbtwn2  32231  cvnbtwn3  32232  cvnbtwn4  32233  dfon2lem3  35759  dfon2lem5  35761  dfon2lem6  35762  dfon2lem7  35763  dfon2lem8  35764  dfon3  35866  lcvbr2  39001  lcvnbtwn2  39006  lcvnbtwn3  39007  rr-phpd  44182