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	⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 𝑧 ∈ 𝑥 ∧ ∀ 𝑦 ∀ 𝑧 𝑦 ∈ 𝑥 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 𝑧 ∈ 𝑥 ∧ ∀ 𝑦 ∀ 𝑧 𝑦 ∈ 𝑥 ) ) ) )