Theorem vtoclg1f 3534

Description: Version of vtoclgf 3533 with one nonfreeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-10 2180 and ax-11 2197. (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 236	. . 3 ⊢ (𝑥 = 𝐴 → 𝜓)
6	2, 5	exlimi 2257	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓)
7	1, 6	syl 18	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-clel 2839

This theorem is used by:  ceqsexg  3610  mob  3678  opeliunxp2  5820  fvopab5  7047  opeliunxp2f  8252  fprodsplit1f  16183  cnextfvval  24411  dvfsumlem2  26374  dvfsumlem4  26376  bnj981  35647  dmrelrnrel  46442  fmul01  46795  fmuldfeq  46798  fmul01lt1lem1  46799  fprodcnlem  46814  stoweidlem3  47216  stoweidlem26  47239  stoweidlem31  47244  stoweidlem43  47256  stoweidlem51  47264  fourierdlem86  47405  fourierdlem89  47408  fourierdlem91  47410  sge0f1o  47595  salpreimagelt  47920  salpreimalegt  47922