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

Metamath Proof Explorer

Theorem sbcg

Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf . (Contributed by Alan Sare, 10-Nov-2012) Reduce axiom usage. (Revised by GG, 12-Oct-2024)

Ref Expression
Assertion sbcg ⊢ A ∈ V → [˙A / x]˙ φ ↔ φ

Proof

Step Hyp Ref Expression
1 df-sbc ⊢ [˙A / x]˙ φ ↔ A ∈ x | φ
2 dfclel ⊢ A ∈ x | φ ↔ ∃ y y = A ∧ y ∈ x | φ
3 df-clab ⊢ y ∈ x | φ ↔ y x φ
4 sbv ⊢ y x φ ↔ φ
5 3 4 bitri ⊢ y ∈ x | φ ↔ φ
6 5 anbi2i ⊢ y = A ∧ y ∈ x | φ ↔ y = A ∧ φ
7 6 exbii ⊢ ∃ y y = A ∧ y ∈ x | φ ↔ ∃ y y = A ∧ φ
8 1 2 7 3bitrri ⊢ ∃ y y = A ∧ φ ↔ [˙A / x]˙ φ
9 dfclel ⊢ A ∈ V ↔ ∃ y y = A ∧ y ∈ V
10 9 biimpi ⊢ A ∈ V → ∃ y y = A ∧ y ∈ V
11 simpr ⊢ y = A ∧ φ → φ
12 11 ax-gen ⊢ ∀ y y = A ∧ φ → φ
13 19.23v ⊢ ∀ y y = A ∧ φ → φ ↔ ∃ y y = A ∧ φ → φ
14 13 biimpi ⊢ ∀ y y = A ∧ φ → φ → ∃ y y = A ∧ φ → φ
15 12 14 mp1i ⊢ ∃ y y = A ∧ y ∈ V → ∃ y y = A ∧ φ → φ
16 2a1 ⊢ y = A → y ∈ V → φ → y = A
17 16 imp ⊢ y = A ∧ y ∈ V → φ → y = A
18 17 ancrd ⊢ y = A ∧ y ∈ V → φ → y = A ∧ φ
19 18 eximi ⊢ ∃ y y = A ∧ y ∈ V → ∃ y φ → y = A ∧ φ
20 19.37imv ⊢ ∃ y φ → y = A ∧ φ → φ → ∃ y y = A ∧ φ
21 19 20 syl ⊢ ∃ y y = A ∧ y ∈ V → φ → ∃ y y = A ∧ φ
22 15 21 impbid ⊢ ∃ y y = A ∧ y ∈ V → ∃ y y = A ∧ φ ↔ φ
23 10 22 syl ⊢ A ∈ V → ∃ y y = A ∧ φ ↔ φ
24 8 23 bitr3id ⊢ A ∈ V → [˙A / x]˙ φ ↔ φ