Theorem vtoclg1f 3516

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548  ∃wex 1787  Ⅎwnf 1791   ∈ wcel 2121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-12 2191

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-nf 1792  df-sb 2075  df-clab 2720  df-clel 2816

This theorem is referenced by:  ceqsexg  3593  mob  3660  opeliunxp2  5783  fvopab5  6973  opeliunxp2f  8154  fprodsplit1f  15950  cnextfvval  24052  dvfsumlem2  26016  dvfsumlem4  26018  bnj981  35147  dmrelrnrel  45685  fmul01  46039  fmuldfeq  46042  fmul01lt1lem1  46043  fprodcnlem  46058  stoweidlem3  46460  stoweidlem26  46483  stoweidlem31  46488  stoweidlem43  46500  stoweidlem51  46508  fourierdlem86  46649  fourierdlem89  46652  fourierdlem91  46654  sge0f1o  46839  salpreimagelt  47164  salpreimalegt  47166