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 ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜑 ) )

Proof

Step Hyp Ref Expression
1 df-sbc ⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝐴 ∈ { 𝑥 ∣ 𝜑 } )
2 dfclel ⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) )
3 df-clab ⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
4 sbv ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 )
5 3 4 bitri ⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 )
6 5 anbi2i ⊢ ( ( 𝑦 = 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) ↔ ( 𝑦 = 𝐴 ∧ 𝜑 ) )
7 6 exbii ⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 ) )
8 1 2 7 3bitrri ⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 ) ↔ [ 𝐴 / 𝑥 ] 𝜑 )
9 dfclel ⊢ ( 𝐴 ∈ 𝑉 ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉 ) )
10 9 biimpi ⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉 ) )
11 simpr ⊢ ( ( 𝑦 = 𝐴 ∧ 𝜑 ) → 𝜑 )
12 11 ax-gen ⊢ ∀ 𝑦 ( ( 𝑦 = 𝐴 ∧ 𝜑 ) → 𝜑 )
13 19.23v ⊢ ( ∀ 𝑦 ( ( 𝑦 = 𝐴 ∧ 𝜑 ) → 𝜑 ) ↔ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 ) → 𝜑 ) )
14 13 biimpi ⊢ ( ∀ 𝑦 ( ( 𝑦 = 𝐴 ∧ 𝜑 ) → 𝜑 ) → ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 ) → 𝜑 ) )
15 12 14 mp1i ⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉 ) → ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 ) → 𝜑 ) )
16 2a1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ 𝑉 → ( 𝜑 → 𝑦 = 𝐴 ) ) )
17 16 imp ⊢ ( ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉 ) → ( 𝜑 → 𝑦 = 𝐴 ) )
18 17 ancrd ⊢ ( ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉 ) → ( 𝜑 → ( 𝑦 = 𝐴 ∧ 𝜑 ) ) )
19 18 eximi ⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉 ) → ∃ 𝑦 ( 𝜑 → ( 𝑦 = 𝐴 ∧ 𝜑 ) ) )
20 19.37imv ⊢ ( ∃ 𝑦 ( 𝜑 → ( 𝑦 = 𝐴 ∧ 𝜑 ) ) → ( 𝜑 → ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 ) ) )
21 19 20 syl ⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉 ) → ( 𝜑 → ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 ) ) )
22 15 21 impbid ⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉 ) → ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 ) ↔ 𝜑 ) )
23 10 22 syl ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 ) ↔ 𝜑 ) )
24 8 23 bitr3id ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜑 ) )