Theorem vtoclg1f 3543

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1568  ∃wex 1807  Ⅎwnf 1811   ∈ wcel 2150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-12 2220

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-nf 1812  df-sb 2099  df-clab 2749  df-clel 2845

This theorem is referenced by:  ceqsexg  3620  mob  3688  opeliunxp2  5828  fvopab5  7027  opeliunxp2f  8209  fprodsplit1f  16047  cnextfvval  24205  dvfsumlem2  26169  dvfsumlem4  26171  bnj981  35308  dmrelrnrel  45894  fmul01  46248  fmuldfeq  46251  fmul01lt1lem1  46252  fprodcnlem  46267  stoweidlem3  46669  stoweidlem26  46692  stoweidlem31  46697  stoweidlem43  46709  stoweidlem51  46717  fourierdlem86  46858  fourierdlem89  46861  fourierdlem91  46863  sge0f1o  47048  salpreimagelt  47373  salpreimalegt  47375