Theorem vtoclg1f 3525

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ∃wex 1781  Ⅎwnf 1785   ∈ wcel 2106

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-clel 2809

This theorem is referenced by:  vtoclgOLDOLD  3528  ceqsexg  3606  elabgOLD  3632  mob  3678  opeliunxp2  5799  fvopab5  6985  opeliunxp2f  8146  fprodsplit1f  15884  cnextfvval  23453  dvfsumlem2  25428  dvfsumlem4  25430  bnj981  33651  dmrelrnrel  43568  fmul01  43941  fmuldfeq  43944  fmul01lt1lem1  43945  stoweidlem3  44364  stoweidlem26  44387  stoweidlem31  44392  stoweidlem43  44404  stoweidlem51  44412  fourierdlem86  44553  fourierdlem89  44556  fourierdlem91  44558  salpreimagelt  45068  salpreimalegt  45070