Metamath Proof Explorer


Theorem eleq2dALT

Description: Alternate proof of eleq2d , shorter at the expense of requiring ax-12 . (Contributed by NM, 27-Dec-1993) (Revised by Wolf Lammen, 20-Nov-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis eleq1d.1 ( 𝜑𝐴 = 𝐵 )
Assertion eleq2dALT ( 𝜑 → ( 𝐶𝐴𝐶𝐵 ) )

Proof

Step Hyp Ref Expression
1 eleq1d.1 ( 𝜑𝐴 = 𝐵 )
2 dfcleq ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) )
3 1 2 sylib ( 𝜑 → ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) )
4 3 19.21bi ( 𝜑 → ( 𝑥𝐴𝑥𝐵 ) )
5 4 anbi2d ( 𝜑 → ( ( 𝑥 = 𝐶𝑥𝐴 ) ↔ ( 𝑥 = 𝐶𝑥𝐵 ) ) )
6 5 exbidv ( 𝜑 → ( ∃ 𝑥 ( 𝑥 = 𝐶𝑥𝐴 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐶𝑥𝐵 ) ) )
7 dfclel ( 𝐶𝐴 ↔ ∃ 𝑥 ( 𝑥 = 𝐶𝑥𝐴 ) )
8 dfclel ( 𝐶𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐶𝑥𝐵 ) )
9 6 7 8 3bitr4g ( 𝜑 → ( 𝐶𝐴𝐶𝐵 ) )