Theorem sbcieg 3783

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ∈ wcel 2141  {cab 2739  [wsbc 3744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-sbc 3745

This theorem is referenced by:  sbcie  3785  2nreu  4397  reuprg0  4660  rabsnif  4681  ralrnmptw  7071  ralrnmpt  7073  fpwwe2lem3  10588  nn1suc  12229  opfi1uzind  14521  mndind  18845  fgcl  23918  cfinfil  23933  csdfil  23934  supfil  23935  fin1aufil  23972  ifeqeqx  32690  nn0min  32973  bnj1452  35311  cdlemk35s  41525  cdlemk39s  41527  cdlemk42  41529  2nn0ind  43486  zindbi  43487  prproropreud  48079