Theorem vtoclg1f 3470

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1542  ∃wex 1786  Ⅎwnf 1790   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-12 2178

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2717  df-clel 2811

This theorem is referenced by:  vtoclgOLD  3472  ceqsexg  3550  elabg  3573  mob  3617  opeliunxp2  5682  fvopab5  6808  opeliunxp2f  7906  fprodsplit1f  15437  cnextfvval  22817  dvfsumlem2  24779  dvfsumlem4  24781  bnj981  32501  dmrelrnrel  42295  fmul01  42655  fmuldfeq  42658  fmul01lt1lem1  42659  stoweidlem3  43078  stoweidlem26  43101  stoweidlem31  43106  stoweidlem43  43118  stoweidlem51  43126  fourierdlem86  43267  fourierdlem89  43270  fourierdlem91  43272  salpreimagelt  43776  salpreimalegt  43778