Theorem vtoclg1f 3569

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539  ∃wex 1778  Ⅎwnf 1782   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-12 2176

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2714  df-clel 2815

This theorem is referenced by:  ceqsexg  3652  mob  3722  opeliunxp2  5848  fvopab5  7048  opeliunxp2f  8236  fprodsplit1f  16027  cnextfvval  24074  dvfsumlem2  26068  dvfsumlem2OLD  26069  dvfsumlem4  26071  bnj981  34965  dmrelrnrel  45236  fmul01  45600  fmuldfeq  45603  fmul01lt1lem1  45604  fprodcnlem  45619  stoweidlem3  46023  stoweidlem26  46046  stoweidlem31  46051  stoweidlem43  46063  stoweidlem51  46071  fourierdlem86  46212  fourierdlem89  46215  fourierdlem91  46217  sge0f1o  46402  salpreimagelt  46727  salpreimalegt  46729