Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  eleq1w Structured version   Visualization version   GIF version

Theorem eleq1w 2872
 Description: Weaker version of eleq1 2877 (but more general than elequ1 2118) not depending on ax-ext 2770 nor df-cleq 2791. Note that this provides a proof of ax-8 2113 from Tarski's FOL and dfclel 2871 (simply consider an instance where 𝐴 is replaced by a setvar and deduce the forward implication by biimpd 232), which shows that dfclel 2871 is too powerful to be used as a definition instead of df-clel 2870. (Contributed by BJ, 24-Jun-2019.)
Assertion
Ref Expression
eleq1w (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))

Proof of Theorem eleq1w
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 equequ2 2033 . . . 4 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
21anbi1d 632 . . 3 (𝑥 = 𝑦 → ((𝑧 = 𝑥𝑧𝐴) ↔ (𝑧 = 𝑦𝑧𝐴)))
32exbidv 1922 . 2 (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥𝑧𝐴) ↔ ∃𝑧(𝑧 = 𝑦𝑧𝐴)))
4 dfclel 2871 . 2 (𝑥𝐴 ↔ ∃𝑧(𝑧 = 𝑥𝑧𝐴))
5 dfclel 2871 . 2 (𝑦𝐴 ↔ ∃𝑧(𝑧 = 𝑦𝑧𝐴))
63, 4, 53bitr4g 317 1 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))