This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ax12wdemo

Description: Example of an application of ax12w that results in an instance of ax-12 for a contrived formula with mixed free and bound variables, ( x e. y /\ A. x z e. x /\ A. y A. z y e. x ) , in place of ph . The proof illustrates bound variable renaming with cbvalvw to obtain fresh variables to avoid distinct variable clashes. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 14-Apr-2017)

Ref Expression
Assertion ax12wdemo ( 𝑥 = 𝑦 → ( ∀ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 𝑧 ∈ 𝑥 ∧ ∀ 𝑦 ∀ 𝑧 𝑦 ∈ 𝑥 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 𝑧 ∈ 𝑥 ∧ ∀ 𝑦 ∀ 𝑧 𝑦 ∈ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 elequ1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑦 ↔ 𝑦 ∈ 𝑦 ) )
2 elequ2 ⊢ ( 𝑥 = 𝑤 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤 ) )
3 2 cbvalvw ⊢ ( ∀ 𝑥 𝑧 ∈ 𝑥 ↔ ∀ 𝑤 𝑧 ∈ 𝑤 )
4 3 a1i ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑥 𝑧 ∈ 𝑥 ↔ ∀ 𝑤 𝑧 ∈ 𝑤 ) )
5 elequ1 ⊢ ( 𝑦 = 𝑣 → ( 𝑦 ∈ 𝑥 ↔ 𝑣 ∈ 𝑥 ) )
6 5 albidv ⊢ ( 𝑦 = 𝑣 → ( ∀ 𝑧 𝑦 ∈ 𝑥 ↔ ∀ 𝑧 𝑣 ∈ 𝑥 ) )
7 6 cbvalvw ⊢ ( ∀ 𝑦 ∀ 𝑧 𝑦 ∈ 𝑥 ↔ ∀ 𝑣 ∀ 𝑧 𝑣 ∈ 𝑥 )
8 elequ2 ⊢ ( 𝑥 = 𝑦 → ( 𝑣 ∈ 𝑥 ↔ 𝑣 ∈ 𝑦 ) )
9 8 albidv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝑣 ∈ 𝑥 ↔ ∀ 𝑧 𝑣 ∈ 𝑦 ) )
10 9 albidv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑣 ∀ 𝑧 𝑣 ∈ 𝑥 ↔ ∀ 𝑣 ∀ 𝑧 𝑣 ∈ 𝑦 ) )
11 7 10 bitrid ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑦 ∀ 𝑧 𝑦 ∈ 𝑥 ↔ ∀ 𝑣 ∀ 𝑧 𝑣 ∈ 𝑦 ) )
12 1 4 11 3anbi123d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 𝑧 ∈ 𝑥 ∧ ∀ 𝑦 ∀ 𝑧 𝑦 ∈ 𝑥 ) ↔ ( 𝑦 ∈ 𝑦 ∧ ∀ 𝑤 𝑧 ∈ 𝑤 ∧ ∀ 𝑣 ∀ 𝑧 𝑣 ∈ 𝑦 ) ) )
13 elequ2 ⊢ ( 𝑦 = 𝑣 → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑣 ) )
14 7 a1i ⊢ ( 𝑦 = 𝑣 → ( ∀ 𝑦 ∀ 𝑧 𝑦 ∈ 𝑥 ↔ ∀ 𝑣 ∀ 𝑧 𝑣 ∈ 𝑥 ) )
15 13 14 3anbi13d ⊢ ( 𝑦 = 𝑣 → ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 𝑧 ∈ 𝑥 ∧ ∀ 𝑦 ∀ 𝑧 𝑦 ∈ 𝑥 ) ↔ ( 𝑥 ∈ 𝑣 ∧ ∀ 𝑥 𝑧 ∈ 𝑥 ∧ ∀ 𝑣 ∀ 𝑧 𝑣 ∈ 𝑥 ) ) )
16 12 15 ax12w ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 𝑧 ∈ 𝑥 ∧ ∀ 𝑦 ∀ 𝑧 𝑦 ∈ 𝑥 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 𝑧 ∈ 𝑥 ∧ ∀ 𝑦 ∀ 𝑧 𝑦 ∈ 𝑥 ) ) ) )