Theorem vtoclg1f 3515

Description: Version of vtoclgf 3514 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 2819	. 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 2716  df-clel 2812

This theorem is referenced by:  ceqsexg  3596  mob  3664  opeliunxp2  5785  fvopab5  6973  opeliunxp2f  8151  fprodsplit1f  15914  cnextfvval  24008  dvfsumlem2  25974  dvfsumlem2OLD  25975  dvfsumlem4  25977  bnj981  35098  dmrelrnrel  45658  fmul01  46014  fmuldfeq  46017  fmul01lt1lem1  46018  fprodcnlem  46033  stoweidlem3  46435  stoweidlem26  46458  stoweidlem31  46463  stoweidlem43  46475  stoweidlem51  46483  fourierdlem86  46624  fourierdlem89  46627  fourierdlem91  46629  sge0f1o  46814  salpreimagelt  47139  salpreimalegt  47141