Theorem vtoclg1f 3553

Description: Version of vtoclgf 3552 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 2809	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2		vtoclg1f.nf	. . 3 ⊢ Ⅎ𝑥𝜓
3		vtoclg1f.min	. . . 4 ⊢ 𝜑
4		vtoclg1f.maj	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
5	3, 4	mpbii 232	. . 3 ⊢ (𝑥 = 𝐴 → 𝜓)
6	2, 5	exlimi 2202	. 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 2163

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2704  df-clel 2804

This theorem is referenced by:  ceqsexg  3636  elabgOLD  3662  mob  3708  opeliunxp2  5832  fvopab5  7024  opeliunxp2f  8196  fprodsplit1f  15940  cnextfvval  23924  dvfsumlem2  25916  dvfsumlem2OLD  25917  dvfsumlem4  25919  bnj981  34490  dmrelrnrel  44494  fmul01  44865  fmuldfeq  44868  fmul01lt1lem1  44869  fprodcnlem  44884  stoweidlem3  45288  stoweidlem26  45311  stoweidlem31  45316  stoweidlem43  45328  stoweidlem51  45336  fourierdlem86  45477  fourierdlem89  45480  fourierdlem91  45482  salpreimagelt  45992  salpreimalegt  45994