Theorem dtruALT2

Description: Alternate proof of dtru using ax-pr instead of ax-pow . (Contributed by Mario Carneiro, 31-Aug-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	dtruALT2	⊢ ¬ ∀ 𝑥 𝑥 = 𝑦

Proof

Step	Hyp	Ref	Expression
1		0inp0	⊢ ( 𝑦 = ∅ → ¬ 𝑦 = { ∅ } )
2		snex	⊢ { ∅ } ∈ V
3		eqeq2	⊢ ( 𝑥 = { ∅ } → ( 𝑦 = 𝑥 ↔ 𝑦 = { ∅ } ) )
4	3	notbid	⊢ ( 𝑥 = { ∅ } → ( ¬ 𝑦 = 𝑥 ↔ ¬ 𝑦 = { ∅ } ) )
5	2 4	spcev	⊢ ( ¬ 𝑦 = { ∅ } → ∃ 𝑥 ¬ 𝑦 = 𝑥 )
6	1 5	syl	⊢ ( 𝑦 = ∅ → ∃ 𝑥 ¬ 𝑦 = 𝑥 )
7		0ex	⊢ ∅ ∈ V
8		eqeq2	⊢ ( 𝑥 = ∅ → ( 𝑦 = 𝑥 ↔ 𝑦 = ∅ ) )
9	8	notbid	⊢ ( 𝑥 = ∅ → ( ¬ 𝑦 = 𝑥 ↔ ¬ 𝑦 = ∅ ) )
10	7 9	spcev	⊢ ( ¬ 𝑦 = ∅ → ∃ 𝑥 ¬ 𝑦 = 𝑥 )
11	6 10	pm2.61i	⊢ ∃ 𝑥 ¬ 𝑦 = 𝑥
12		exnal	⊢ ( ∃ 𝑥 ¬ 𝑦 = 𝑥 ↔ ¬ ∀ 𝑥 𝑦 = 𝑥 )
13		eqcom	⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 )
14	13	albii	⊢ ( ∀ 𝑥 𝑦 = 𝑥 ↔ ∀ 𝑥 𝑥 = 𝑦 )
15	12 14	xchbinx	⊢ ( ∃ 𝑥 ¬ 𝑦 = 𝑥 ↔ ¬ ∀ 𝑥 𝑥 = 𝑦 )
16	11 15	mpbi	⊢ ¬ ∀ 𝑥 𝑥 = 𝑦