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

Metamath Proof Explorer

Theorem bnj1468

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1468.1 ⊢ ψ → ∀ x ψ
bnj1468.2 ⊢ x = A → φ ↔ ψ
bnj1468.3 ⊢ y ∈ A → ∀ x y ∈ A
Assertion bnj1468 ⊢ A ∈ V → [˙A / x]˙ φ ↔ ψ

Proof

Step Hyp Ref Expression
1 bnj1468.1 ⊢ ψ → ∀ x ψ
2 bnj1468.2 ⊢ x = A → φ ↔ ψ
3 bnj1468.3 ⊢ y ∈ A → ∀ x y ∈ A
4 sbccow ⊢ [˙A / y]˙ [˙y / x]˙ φ ↔ [˙A / x]˙ φ
5 ax-5 ⊢ ψ → ∀ y ψ
6 3 nfcii ⊢ Ⅎ _ x A
7 6 nfeq2 ⊢ Ⅎ x y = A
8 nfsbc1v ⊢ Ⅎ x [˙y / x]˙ φ
9 1 nf5i ⊢ Ⅎ x ψ
10 8 9 nfbi ⊢ Ⅎ x [˙y / x]˙ φ ↔ ψ
11 7 10 nfim ⊢ Ⅎ x y = A → [˙y / x]˙ φ ↔ ψ
12 11 nf5ri ⊢ y = A → [˙y / x]˙ φ ↔ ψ → ∀ x y = A → [˙y / x]˙ φ ↔ ψ
13 ax6ev ⊢ ∃ x x = y
14 eqeq1 ⊢ x = y → x = A ↔ y = A
15 14 2 biimtrrdi ⊢ x = y → y = A → φ ↔ ψ
16 sbceq1a ⊢ x = y → φ ↔ [˙y / x]˙ φ
17 16 bibi1d ⊢ x = y → φ ↔ ψ ↔ [˙y / x]˙ φ ↔ ψ
18 15 17 sylibd ⊢ x = y → y = A → [˙y / x]˙ φ ↔ ψ
19 13 18 bnj101 ⊢ ∃ x y = A → [˙y / x]˙ φ ↔ ψ
20 12 19 bnj1131 ⊢ y = A → [˙y / x]˙ φ ↔ ψ
21 5 20 bnj1464 ⊢ A ∈ V → [˙A / y]˙ [˙y / x]˙ φ ↔ ψ
22 4 21 bitr3id ⊢ A ∈ V → [˙A / x]˙ φ ↔ ψ