Theorem vtoclg1f 3494

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-clel 2817

This theorem is referenced by:  vtoclgOLD  3496  ceqsexg  3575  elabgOLD  3601  mob  3647  opeliunxp2  5736  fvopab5  6889  opeliunxp2f  7997  fprodsplit1f  15628  cnextfvval  23124  dvfsumlem2  25096  dvfsumlem4  25098  bnj981  32830  dmrelrnrel  42654  fmul01  43011  fmuldfeq  43014  fmul01lt1lem1  43015  stoweidlem3  43434  stoweidlem26  43457  stoweidlem31  43462  stoweidlem43  43474  stoweidlem51  43482  fourierdlem86  43623  fourierdlem89  43626  fourierdlem91  43628  salpreimagelt  44132  salpreimalegt  44134