Theorem dfpss2 4088

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1540   ≠ wne 2940   ⊆ wss 3951   ⊊ wpss 3952

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 2941  df-pss 3971

This theorem is referenced by:  dfpss3  4089  sspss  4102  psstr  4107  npss  4113  ssnelpss  4114  pssv  4449  disj4  4459  f1imapss  7286  pssnn  9208  phpeqd  9252  phpeqdOLD  9262  nnsdomo  9270  inf3lem6  9673  ssfin4  10350  fin23lem25  10364  fin23lem38  10389  isf32lem2  10394  pwfseqlem4  10702  genpcl  11048  prlem934  11073  ltaddpr  11074  sltlpss  27945  chnlei  31504  cvbr2  32302  cvnbtwn2  32306  cvnbtwn3  32307  cvnbtwn4  32308  dfon2lem3  35786  dfon2lem5  35788  dfon2lem6  35789  dfon2lem7  35790  dfon2lem8  35791  dfon3  35893  lcvbr2  39023  lcvnbtwn2  39028  lcvnbtwn3  39029  rr-phpd  44222