Theorem sbcieg 3786

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 3748	. 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
2		sbcieg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	elabg 3638	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	1, 3	bitrid 286	1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   ∈ wcel 2145  {cab 2743  [wsbc 3747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-sbc 3748

This theorem is referenced by:  sbcie  3788  2nreu  4401  reuprg0  4664  rabsnif  4685  ralrnmptw  7079  ralrnmpt  7081  fpwwe2lem3  10606  nn1suc  12246  opfi1uzind  14538  mndind  18877  fgcl  23996  cfinfil  24011  csdfil  24012  supfil  24013  fin1aufil  24050  ifeqeqx  32798  nn0min  33078  bnj1452  35357  cdlemk35s  41573  cdlemk39s  41575  cdlemk42  41577  2nn0ind  43534  zindbi  43535  prproropreud  48113