Theorem vtoclg1f 3522

Description: Version of vtoclgf 3521 with one nonfreeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-10 2144 and ax-11 2160. (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 233	. . 3 ⊢ (𝑥 = 𝐴 → 𝜓)
6	2, 5	exlimi 2220	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓)
7	1, 6	syl 17	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ∃wex 1780  Ⅎwnf 1784   ∈ wcel 2111

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 1968  ax-7 2009  ax-8 2113  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-clel 2806

This theorem is referenced by:  ceqsexg  3603  mob  3671  opeliunxp2  5777  fvopab5  6962  opeliunxp2f  8140  fprodsplit1f  15897  cnextfvval  23980  dvfsumlem2  25960  dvfsumlem2OLD  25961  dvfsumlem4  25963  bnj981  34962  dmrelrnrel  45322  fmul01  45679  fmuldfeq  45682  fmul01lt1lem1  45683  fprodcnlem  45698  stoweidlem3  46100  stoweidlem26  46123  stoweidlem31  46128  stoweidlem43  46140  stoweidlem51  46148  fourierdlem86  46289  fourierdlem89  46292  fourierdlem91  46294  sge0f1o  46479  salpreimagelt  46804  salpreimalegt  46806