Theorem vtoclg1f 3528

Description: Version of vtoclgf 3527 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  3609  mob  3677  opeliunxp2  5797  fvopab5  6985  opeliunxp2f  8164  fprodsplit1f  15927  cnextfvval  24026  dvfsumlem2  26006  dvfsumlem2OLD  26007  dvfsumlem4  26009  bnj981  35132  dmrelrnrel  45613  fmul01  45969  fmuldfeq  45972  fmul01lt1lem1  45973  fprodcnlem  45988  stoweidlem3  46390  stoweidlem26  46413  stoweidlem31  46418  stoweidlem43  46430  stoweidlem51  46438  fourierdlem86  46579  fourierdlem89  46582  fourierdlem91  46584  sge0f1o  46769  salpreimagelt  47094  salpreimalegt  47096