Theorem vtoclg1f 3534

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  ∃wex 1808  Ⅎwnf 1812   ∈ wcel 2142

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-nf 1813  df-sb 2096  df-clab 2741  df-clel 2837

This theorem is used by:  ceqsexg  3611  mob  3679  opeliunxp2  5823  fvopab5  7023  opeliunxp2f  8204  fprodsplit1f  16051  cnextfvval  24233  dvfsumlem2  26197  dvfsumlem4  26199  bnj981  35347  dmrelrnrel  45970  fmul01  46324  fmuldfeq  46327  fmul01lt1lem1  46328  fprodcnlem  46343  stoweidlem3  46745  stoweidlem26  46768  stoweidlem31  46773  stoweidlem43  46785  stoweidlem51  46793  fourierdlem86  46934  fourierdlem89  46937  fourierdlem91  46939  sge0f1o  47124  salpreimagelt  47449  salpreimalegt  47451