Theorem sbcieg 3786

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 10-Nov-2005.) Avoid ax-10 2179, ax-12 2216. (Revised by GG, 12-Oct-2024.)

Hypothesis

Ref	Expression
sbcieg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
sbcieg	⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem sbcieg

Step	Hyp	Ref	Expression
1		df-sbc 3748	. 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
2		sbcieg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	elabg 3638	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	1, 3	bitrid 286	1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  {cab 2744  [wsbc 3747

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-sbc 3748

This theorem is used by:  sbcie  3788  2nreu  4412  reuprg0  4673  rabsnif  4694  ralrnmptw  7096  ralrnmpt  7098  fpwwe2lem3  10636  nn1suc  12273  opfi1uzind  14568  mndind  18918  fgcl  24072  cfinfil  24087  csdfil  24088  supfil  24089  fin1aufil  24126  ifeqeqx  32925  nn0min  33202  bnj1452  35472  cdlemk35s  41752  cdlemk39s  41754  cdlemk42  41756  2nn0ind  43713  zindbi  43714  prproropreud  48299