Theorem vtoclgaf 3542

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 2943	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
3		vtoclgaf.2	. . . 4 ⊢ Ⅎ𝑥𝜓
4	2, 3	nfim 1929	. . 3 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
5		eleq1 2853	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		vtoclgaf.3	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
7	5, 6	imbi12d 347	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
8		vtoclgaf.4	. . 3 ⊢ (𝑥 ∈ 𝐵 → 𝜑)
9	1, 4, 7, 8	vtoclgf 3536	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 → 𝜓))
10	9	pm2.43i 53	1 ⊢ (𝐴 ∈ 𝐵 → 𝜓)

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

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-v 3459

This theorem is used by:  vtocl2gaf  3545  vtocl3gaf  3546  ssiun2s  5015  iunopeqop  5506  iunopeqopOLD  5507  fvmptss  7006  fvmptf  7015  fmptco  7129  tfis  7857  inar1  10779  sumss  15802  fprodn0  16060  prmind2  16769  lss1d  21138  itg2splitlem  25962  dgrle  26455  cnlnadjlem5  32498  poimirlem25  38357  stoweidlem26  46817