Theorem vtoclg1f 3525

Description: Version of vtoclgf 3524 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 2817	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2		vtoclg1f.nf	. . 3 ⊢ Ⅎ𝑥𝜓
3		vtoclg1f.min	. . . 4 ⊢ 𝜑
4		vtoclg1f.maj	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
5	3, 4	mpbii 233	. . 3 ⊢ (𝑥 = 𝐴 → 𝜓)
6	2, 5	exlimi 2223	. 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 2183

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 2714  df-clel 2810

This theorem is referenced by:  ceqsexg  3606  mob  3674  opeliunxp2  5786  fvopab5  6974  opeliunxp2f  8152  fprodsplit1f  15915  cnextfvval  24011  dvfsumlem2  25991  dvfsumlem2OLD  25992  dvfsumlem4  25994  bnj981  35085  dmrelrnrel  45507  fmul01  45863  fmuldfeq  45866  fmul01lt1lem1  45867  fprodcnlem  45882  stoweidlem3  46284  stoweidlem26  46307  stoweidlem31  46312  stoweidlem43  46324  stoweidlem51  46332  fourierdlem86  46473  fourierdlem89  46476  fourierdlem91  46478  sge0f1o  46663  salpreimagelt  46988  salpreimalegt  46990