Theorem vtoclg1f 3556

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533  ∃wex 1773  Ⅎwnf 1777   ∈ wcel 2098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-12 2166

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2705  df-clel 2805

This theorem is referenced by:  ceqsexg  3639  elabgOLD  3666  mob  3712  opeliunxp2  5843  fvopab5  7041  opeliunxp2f  8220  fprodsplit1f  15972  cnextfvval  23987  dvfsumlem2  25979  dvfsumlem2OLD  25980  dvfsumlem4  25982  bnj981  34586  dmrelrnrel  44602  fmul01  44970  fmuldfeq  44973  fmul01lt1lem1  44974  fprodcnlem  44989  stoweidlem3  45393  stoweidlem26  45416  stoweidlem31  45421  stoweidlem43  45433  stoweidlem51  45441  fourierdlem86  45582  fourierdlem89  45585  fourierdlem91  45587  salpreimagelt  46097  salpreimalegt  46099