Theorem vtoclgaf 3535

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 17-Feb-2006.) (Revised by Mario Carneiro, 10-Oct-2016.)

Hypotheses

Ref	Expression
vtoclgaf.1	⊢ Ⅎ𝑥𝐴
vtoclgaf.2	⊢ Ⅎ𝑥𝜓
vtoclgaf.3	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
vtoclgaf.4	⊢ (𝑥 ∈ 𝐵 → 𝜑)

Assertion

Ref	Expression
vtoclgaf	⊢ (𝐴 ∈ 𝐵 → 𝜓)

Distinct variable group:   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem vtoclgaf

Step	Hyp	Ref	Expression
1		vtoclgaf.1	. . 3 ⊢ Ⅎ𝑥𝐴
2	1	nfel1 2938	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
3		vtoclgaf.2	. . . 4 ⊢ Ⅎ𝑥𝜓
4	2, 3	nfim 1929	. . 3 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
5		eleq1 2848	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		vtoclgaf.3	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
7	5, 6	imbi12d 347	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
8		vtoclgaf.4	. . 3 ⊢ (𝑥 ∈ 𝐵 → 𝜑)
9	1, 4, 7, 8	vtoclgf 3529	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 → 𝜓))
10	9	pm2.43i 53	1 ⊢ (𝐴 ∈ 𝐵 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  Ⅎwnf 1816   ∈ wcel 2145  Ⅎwnfc 2907

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-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-v 3452

This theorem is used by:  vtocl2gaf  3538  vtocl3gaf  3539  ssiun2s  5007  iunopeqop  5498  iunopeqopOLD  5499  fvmptss  7000  fvmptf  7009  fmptco  7124  tfis  7852  inar1  10787  sumss  15813  fprodn0  16069  prmind2  16778  lss1d  21150  itg2splitlem  25979  dgrle  26472  cnlnadjlem5  32555  poimirlem25  38397  stoweidlem26  46857