Theorem vtoclg1f 3238

Description: Version of vtoclgf 3237 with one non-freeness hypothesis replaced with a dv condition, thus avoiding dependency on ax-11 2021 and ax-13 2234. (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 3185	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		isset 3180	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
3		vtoclg1f.nf	. . . 4 ⊢ Ⅎ𝑥𝜓
4		vtoclg1f.min	. . . . 5 ⊢ 𝜑
5		vtoclg1f.maj	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
6	4, 5	mpbii 222	. . . 4 ⊢ (𝑥 = 𝐴 → 𝜓)
7	3, 6	exlimi 2073	. . 3 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓)
8	2, 7	sylbi 206	. 2 ⊢ (𝐴 ∈ V → 𝜓)
9	1, 8	syl 17	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ∃wex 1695  Ⅎwnf 1699   ∈ wcel 1977  Vcvv 3173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175

This theorem is referenced by:  vtoclg  3239  ceqsexg  3304  mob  3355  opeliunxp2  5182  fvopab5  6217  opeliunxp2f  7223  cnextfvval  21679  dvfsumlem2  23594  dvfsumlem4  23596  bnj981  30274  fmul01  38647  fmuldfeq  38650  fmul01lt1lem1  38651  cncfiooicclem1  38779  stoweidlem3  38896  stoweidlem26  38919  stoweidlem31  38924  stoweidlem43  38936  stoweidlem51  38944  fourierdlem86  39085  fourierdlem89  39088  fourierdlem91  39090