Theorem vtoclg1f 3514

Description: Version of vtoclgf 3513 with one non-freeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-11 2158 and ax-13 2379. (Contributed by BJ, 1-May-2019.)

Hypotheses

Ref	Expression
vtoclg1f.nf	⊢ Ⅎ𝑥𝜓
vtoclg1f.maj	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
vtoclg1f.min	⊢ 𝜑

Assertion

Ref	Expression
vtoclg1f	⊢ (𝐴 ∈ 𝑉 → 𝜓)

Distinct variable group:   𝑥,𝐴

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

Proof of Theorem vtoclg1f

Step	Hyp	Ref	Expression
1		elisset 3452	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2		vtoclg1f.nf	. . 3 ⊢ Ⅎ𝑥𝜓
3		vtoclg1f.min	. . . 4 ⊢ 𝜑
4		vtoclg1f.maj	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
5	3, 4	mpbii 236	. . 3 ⊢ (𝑥 = 𝐴 → 𝜓)
6	2, 5	exlimi 2215	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓)
7	1, 6	syl 17	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ∃wex 1781  Ⅎwnf 1785   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-cleq 2791  df-clel 2870

This theorem is referenced by:  vtoclgOLD  3516  ceqsexg  3594  elabg  3614  mob  3656  opeliunxp2  5673  fvopab5  6777  opeliunxp2f  7859  fprodsplit1f  15336  cnextfvval  22670  dvfsumlem2  24630  dvfsumlem4  24632  bnj981  32332  dmrelrnrel  41856  fmul01  42222  fmuldfeq  42225  fmul01lt1lem1  42226  stoweidlem3  42645  stoweidlem26  42668  stoweidlem31  42673  stoweidlem43  42685  stoweidlem51  42693  fourierdlem86  42834  fourierdlem89  42837  fourierdlem91  42839  salpreimagelt  43343  salpreimalegt  43345