Theorem dfpss2 4025

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 3911	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2		df-ne 2946	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	anbi2i 623	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
4	1, 3	bitri 274	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 396   = wceq 1542   ≠ wne 2945   ⊆ wss 3892   ⊊ wpss 3893

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 206  df-an 397  df-ne 2946  df-pss 3911

This theorem is referenced by:  dfpss3  4026  sspss  4039  psstr  4044  npss  4050  ssnelpss  4051  pssv  4386  disj4  4398  f1imapss  7136  pssnn  8933  phpeqd  8979  phpeqdOLD  8990  nnsdomo  8997  pssnnOLD  9018  inf3lem6  9369  ssfin4  10067  fin23lem25  10081  fin23lem38  10106  isf32lem2  10111  pwfseqlem4  10419  genpcl  10765  prlem934  10790  ltaddpr  10791  chnlei  29843  cvbr2  30641  cvnbtwn2  30645  cvnbtwn3  30646  cvnbtwn4  30647  dfon2lem3  33757  dfon2lem5  33759  dfon2lem6  33760  dfon2lem7  33761  dfon2lem8  33762  sltlpss  34083  dfon3  34190  lcvbr2  37032  lcvnbtwn2  37037  lcvnbtwn3  37038  rr-phpd  41791