Theorem vtoclg1f 3533

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∃wex 1812  Ⅎwnf 1816   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-12 2215

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2741  df-clel 2837

This theorem is used by:  ceqsexg  3610  mob  3678  opeliunxp2  5822  fvopab5  7024  opeliunxp2f  8212  fprodsplit1f  16083  cnextfvval  24297  dvfsumlem2  26261  dvfsumlem4  26263  bnj981  35467  dmrelrnrel  46064  fmul01  46418  fmuldfeq  46421  fmul01lt1lem1  46422  fprodcnlem  46437  stoweidlem3  46839  stoweidlem26  46862  stoweidlem31  46867  stoweidlem43  46879  stoweidlem51  46887  fourierdlem86  47028  fourierdlem89  47031  fourierdlem91  47033  sge0f1o  47218  salpreimagelt  47543  salpreimalegt  47545