Theorem vtocl2g 3510

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.) Remove dependency on ax-10 2137, ax-11 2154, and ax-13 2372. (Revised by Steven Nguyen, 29-Nov-2022.)

Hypotheses

Ref	Expression
vtocl2g.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
vtocl2g.2	⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))
vtocl2g.3	⊢ 𝜑

Assertion

Ref	Expression
vtocl2g	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒)

Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝑦,𝐵   𝜓,𝑥   𝜒,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)   𝜒(𝑥)   𝐵(𝑥)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem vtocl2g

Step	Hyp	Ref	Expression
1		elex 3450	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		vtocl2g.2	. . . 4 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))
3	2	imbi2d 341	. . 3 ⊢ (𝑦 = 𝐵 → ((𝐴 ∈ V → 𝜓) ↔ (𝐴 ∈ V → 𝜒)))
4		vtocl2g.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
5		vtocl2g.3	. . . 4 ⊢ 𝜑
6	4, 5	vtoclg 3505	. . 3 ⊢ (𝐴 ∈ V → 𝜓)
7	3, 6	vtoclg 3505	. 2 ⊢ (𝐵 ∈ 𝑊 → (𝐴 ∈ V → 𝜒))
8	1, 7	mpan9 507	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  Vcvv 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434

This theorem is referenced by:  vtocl3g  3511  vtocl4g  3519  uniprgOLD  4859  intprgOLD  4915  opthg  5392  opelopabsb  5443  vtoclr  5650  elimasngOLD  5998  funopg  6468  f1osng  6757  fsng  7009  fnpr2g  7086  unexb  7598  op1stg  7843  op2ndg  7844  xpsneng  8843  xpcomeng  8851  sbth  8880  sbthfi  8985  unxpdom  9030  fpwwe2lem4  10390  prcdnq  10749  mhmlem  18695  carsgmon  32281  brimageg  34229  brdomaing  34237  brrangeg  34238  rankung  34468  mbfresfi  35823  zindbi  40768  2sbc6g  42033  2sbc5g  42034  fmulcl  43122