Theorem vtoclg1f 3537

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1562  ∃wex 1801  Ⅎwnf 1805   ∈ wcel 2144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-12 2214

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-nf 1806  df-sb 2093  df-clab 2743  df-clel 2839

This theorem is referenced by:  ceqsexg  3614  mob  3682  opeliunxp2  5812  fvopab5  7011  opeliunxp2f  8192  fprodsplit1f  16022  cnextfvval  24127  dvfsumlem2  26091  dvfsumlem4  26093  bnj981  35247  dmrelrnrel  45807  fmul01  46161  fmuldfeq  46164  fmul01lt1lem1  46165  fprodcnlem  46180  stoweidlem3  46582  stoweidlem26  46605  stoweidlem31  46610  stoweidlem43  46622  stoweidlem51  46630  fourierdlem86  46771  fourierdlem89  46774  fourierdlem91  46776  sge0f1o  46961  salpreimagelt  47286  salpreimalegt  47288