Theorem vtoclg1f 3514

Description: Version of vtoclgf 3513 with one nonfreeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-10 2147 and ax-11 2163. (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 2818	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2		vtoclg1f.nf	. . 3 ⊢ Ⅎ𝑥𝜓
3		vtoclg1f.min	. . . 4 ⊢ 𝜑
4		vtoclg1f.maj	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
5	3, 4	mpbii 233	. . 3 ⊢ (𝑥 = 𝐴 → 𝜓)
6	2, 5	exlimi 2225	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓)
7	1, 6	syl 17	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ∃wex 1781  Ⅎwnf 1785   ∈ wcel 2114

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-clel 2811

This theorem is referenced by:  ceqsexg  3595  mob  3663  opeliunxp2  5793  fvopab5  6981  opeliunxp2f  8160  fprodsplit1f  15955  cnextfvval  24030  dvfsumlem2  25994  dvfsumlem4  25996  bnj981  35092  dmrelrnrel  45655  fmul01  46010  fmuldfeq  46013  fmul01lt1lem1  46014  fprodcnlem  46029  stoweidlem3  46431  stoweidlem26  46454  stoweidlem31  46459  stoweidlem43  46471  stoweidlem51  46479  fourierdlem86  46620  fourierdlem89  46623  fourierdlem91  46625  sge0f1o  46810  salpreimagelt  47135  salpreimalegt  47137