Metamath Proof Explorer

Theorem iseqsetv-clel

Description: Alternate proof of iseqsetv-cleq . The expression E. x x = A does not depend on a particular choice of the set variable. Use this theorem in contexts where df-cleq or ax-ext is not referenced elsewhere in your proof. It is proven from a specific implementation (class builder, axiom df-clab ) of the primitive term x e. A . (Contributed by BJ, 29-Apr-2019) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	iseqsetv-clel	⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ ∃ 𝑦 𝑦 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		issettru	⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ { 𝑧 ∣ ⊤ } )
2		issettru	⊢ ( ∃ 𝑦 𝑦 = 𝐴 ↔ 𝐴 ∈ { 𝑧 ∣ ⊤ } )
3	1 2	bitr4i	⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ ∃ 𝑦 𝑦 = 𝐴 )