Theorem vtoclg1f 3570

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ∃wex 1776  Ⅎwnf 1780   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-12 2175

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-clel 2814

This theorem is referenced by:  ceqsexg  3653  elabgOLD  3678  mob  3726  opeliunxp2  5852  fvopab5  7049  opeliunxp2f  8234  fprodsplit1f  16023  cnextfvval  24089  dvfsumlem2  26082  dvfsumlem2OLD  26083  dvfsumlem4  26085  bnj981  34943  dmrelrnrel  45169  fmul01  45536  fmuldfeq  45539  fmul01lt1lem1  45540  fprodcnlem  45555  stoweidlem3  45959  stoweidlem26  45982  stoweidlem31  45987  stoweidlem43  45999  stoweidlem51  46007  fourierdlem86  46148  fourierdlem89  46151  fourierdlem91  46153  sge0f1o  46338  salpreimagelt  46663  salpreimalegt  46665