Theorem vtoclg1f 3466

Description: Version of vtoclgf 3465 with one non-freeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-11 2150 and ax-13 2334. (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		elex 3414	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		isset 3409	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
3		vtoclg1f.nf	. . . 4 ⊢ Ⅎ𝑥𝜓
4		vtoclg1f.min	. . . . 5 ⊢ 𝜑
5		vtoclg1f.maj	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
6	4, 5	mpbii 225	. . . 4 ⊢ (𝑥 = 𝐴 → 𝜓)
7	3, 6	exlimi 2203	. . 3 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓)
8	2, 7	sylbi 209	. 2 ⊢ (𝐴 ∈ V → 𝜓)
9	1, 8	syl 17	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1601  ∃wex 1823  Ⅎwnf 1827   ∈ wcel 2107  Vcvv 3398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-v 3400

This theorem is referenced by:  vtoclg  3467  ceqsexg  3537  elabg  3556  mob  3600  opeliunxp2  5506  fvopab5  6572  opeliunxp2f  7618  fprodsplit1f  15123  cnextfvval  22277  dvfsumlem2  24227  dvfsumlem4  24229  bnj981  31619  dmrelrnrel  40340  fmul01  40720  fmuldfeq  40723  fmul01lt1lem1  40724  stoweidlem3  41147  stoweidlem26  41170  stoweidlem31  41175  stoweidlem43  41187  stoweidlem51  41195  fourierdlem86  41336  fourierdlem89  41339  fourierdlem91  41341