Theorem vtoclg1f 3530

Description: Version of vtoclgf 3529 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 2842	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2		vtoclg1f.nf	. . 3 ⊢ Ⅎ𝑥𝜓
3		vtoclg1f.min	. . . 4 ⊢ 𝜑
4		vtoclg1f.maj	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
5	3, 4	mpbii 236	. . 3 ⊢ (𝑥 = 𝐴 → 𝜓)
6	2, 5	exlimi 2253	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓)
7	1, 6	syl 18	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  ∃wex 1811  Ⅎwnf 1815   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-clel 2835

This theorem is used by:  ceqsexg  3606  mob  3674  opeliunxp2  5814  fvopab5  7027  opeliunxp2f  8227  fprodsplit1f  16157  cnextfvval  24384  dvfsumlem2  26347  dvfsumlem4  26349  bnj981  35580  dmrelrnrel  46239  fmul01  46592  fmuldfeq  46595  fmul01lt1lem1  46596  fprodcnlem  46611  stoweidlem3  47013  stoweidlem26  47036  stoweidlem31  47041  stoweidlem43  47053  stoweidlem51  47061  fourierdlem86  47202  fourierdlem89  47205  fourierdlem91  47207  sge0f1o  47392  salpreimagelt  47717  salpreimalegt  47719