Theorem vtoclg1f 3525

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∃wex 1779  Ⅎwnf 1783   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-clel 2803

This theorem is referenced by:  ceqsexg  3608  mob  3677  opeliunxp2  5781  fvopab5  6963  opeliunxp2f  8143  fprodsplit1f  15897  cnextfvval  23950  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsumlem4  25934  bnj981  34923  dmrelrnrel  45214  fmul01  45571  fmuldfeq  45574  fmul01lt1lem1  45575  fprodcnlem  45590  stoweidlem3  45994  stoweidlem26  46017  stoweidlem31  46022  stoweidlem43  46034  stoweidlem51  46042  fourierdlem86  46183  fourierdlem89  46186  fourierdlem91  46188  sge0f1o  46373  salpreimagelt  46698  salpreimalegt  46700