Theorem vtoclgaf 3564

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 2917	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
3		vtoclgaf.2	. . . 4 ⊢ Ⅎ𝑥𝜓
4	2, 3	nfim 1897	. . 3 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
5		eleq1 2819	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		vtoclgaf.3	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
7	5, 6	imbi12d 343	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
8		vtoclgaf.4	. . 3 ⊢ (𝑥 ∈ 𝐵 → 𝜑)
9	1, 4, 7, 8	vtoclgf 3556	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 → 𝜓))
10	9	pm2.43i 52	1 ⊢ (𝐴 ∈ 𝐵 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  Ⅎwnf 1783   ∈ wcel 2104  Ⅎwnfc 2881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-v 3474

This theorem is referenced by:  ssiun2s  5050  iunopeqop  5520  fvmptss  7009  fvmptf  7018  fmptco  7128  tfis  7846  inar1  10772  sumss  15674  fprodn0  15927  prmind2  16626  lss1d  20718  itg2splitlem  25498  dgrle  25992  cnlnadjlem5  31591  poimirlem25  36816  stoweidlem26  45040