Theorem sbcieg 3781

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 10-Nov-2005.) Avoid ax-10 2178, ax-12 2215. (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 3743	. 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
2		sbcieg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	elabg 3633	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	1, 3	bitrid 286	1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  {cab 2740  [wsbc 3742

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 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-sbc 3743

This theorem is used by:  sbcie  3783  2nreu  4405  reuprg0  4666  rabsnif  4687  ralrnmptw  7091  ralrnmpt  7093  fpwwe2lem3  10646  nn1suc  12283  opfi1uzind  14580  mndind  18943  fgcl  24110  cfinfil  24125  csdfil  24126  supfil  24127  fin1aufil  24164  ifeqeqx  33025  nn0min  33299  bnj1452  35569  cdlemk35s  41818  cdlemk39s  41820  cdlemk42  41822  2nn0ind  43794  zindbi  43795  prproropreud  48417