Theorem vtoclg1f 3558

Description: Version of vtoclgf 3557 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 2811	. 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 2706  df-clel 2806

This theorem is referenced by:  ceqsexg  3641  elabgOLD  3668  mob  3714  opeliunxp2  5845  fvopab5  7043  opeliunxp2f  8224  fprodsplit1f  15976  cnextfvval  23997  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsumlem4  25992  bnj981  34622  dmrelrnrel  44647  fmul01  45015  fmuldfeq  45018  fmul01lt1lem1  45019  fprodcnlem  45034  stoweidlem3  45438  stoweidlem26  45461  stoweidlem31  45466  stoweidlem43  45478  stoweidlem51  45486  fourierdlem86  45627  fourierdlem89  45630  fourierdlem91  45632  salpreimagelt  46142  salpreimalegt  46144