Theorem vtoclg1f 3557

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∃wex 1779  Ⅎwnf 1783   ∈ wcel 2104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-12 2169

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-clel 2808

This theorem is referenced by:  vtoclgOLDOLD  3559  ceqsexg  3640  elabgOLD  3666  mob  3712  opeliunxp2  5837  fvopab5  7029  opeliunxp2f  8197  fprodsplit1f  15938  cnextfvval  23789  dvfsumlem2  25779  dvfsumlem4  25781  bnj981  34259  gg-dvfsumlem2  35469  dmrelrnrel  44223  fmul01  44594  fmuldfeq  44597  fmul01lt1lem1  44598  stoweidlem3  45017  stoweidlem26  45040  stoweidlem31  45045  stoweidlem43  45057  stoweidlem51  45065  fourierdlem86  45206  fourierdlem89  45209  fourierdlem91  45211  salpreimagelt  45721  salpreimalegt  45723