Theorem vtoclg1f 3568

Description: Version of vtoclgf 3567 with one non-freeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-11 2161 and ax-13 2390. (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 3507	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2		vtoclg1f.nf	. . 3 ⊢ Ⅎ𝑥𝜓
3		vtoclg1f.min	. . . 4 ⊢ 𝜑
4		vtoclg1f.maj	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
5	3, 4	mpbii 235	. . 3 ⊢ (𝑥 = 𝐴 → 𝜓)
6	2, 5	exlimi 2217	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓)
7	1, 6	syl 17	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  ∃wex 1780  Ⅎwnf 1784   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-cleq 2816  df-clel 2895

This theorem is referenced by:  vtoclgOLD  3570  ceqsexg  3648  elabg  3668  mob  3710  opeliunxp2  5711  fvopab5  6802  opeliunxp2f  7878  fprodsplit1f  15346  cnextfvval  22675  dvfsumlem2  24626  dvfsumlem4  24628  bnj981  32224  dmrelrnrel  41497  fmul01  41868  fmuldfeq  41871  fmul01lt1lem1  41872  stoweidlem3  42295  stoweidlem26  42318  stoweidlem31  42323  stoweidlem43  42335  stoweidlem51  42343  fourierdlem86  42484  fourierdlem89  42487  fourierdlem91  42489  salpreimagelt  42993  salpreimalegt  42995