Theorem vtoclg1f 3504

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∃wex 1782  Ⅎwnf 1786   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-clel 2816

This theorem is referenced by:  vtoclgOLD  3506  ceqsexg  3583  elabgOLD  3608  mob  3652  opeliunxp2  5747  fvopab5  6907  opeliunxp2f  8026  fprodsplit1f  15700  cnextfvval  23216  dvfsumlem2  25191  dvfsumlem4  25193  bnj981  32930  dmrelrnrel  42765  fmul01  43121  fmuldfeq  43124  fmul01lt1lem1  43125  stoweidlem3  43544  stoweidlem26  43567  stoweidlem31  43572  stoweidlem43  43584  stoweidlem51  43592  fourierdlem86  43733  fourierdlem89  43736  fourierdlem91  43738  salpreimagelt  44244  salpreimalegt  44246