Theorem vtocl2g 3540

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.) Remove dependency on ax-10 2142, ax-11 2158, and ax-13 2370. (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 3468	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		vtocl2g.2	. . . 4 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))
3	2	imbi2d 340	. . 3 ⊢ (𝑦 = 𝐵 → ((𝐴 ∈ V → 𝜓) ↔ (𝐴 ∈ V → 𝜒)))
4		vtocl2g.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
5		vtocl2g.3	. . . 4 ⊢ 𝜑
6	4, 5	vtoclg 3520	. . 3 ⊢ (𝐴 ∈ V → 𝜓)
7	3, 6	vtoclg 3520	. 2 ⊢ (𝐵 ∈ 𝑊 → (𝐴 ∈ V → 𝜒))
8	1, 7	mpan9 506	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449

This theorem is referenced by:  vtocl3g  3541  vtocl4g  3551  opthg  5437  opelopabsb  5490  vtoclr  5701  funopg  6550  f1osng  6841  fsng  7109  fnpr2g  7184  unexbOLD  7724  op1stg  7980  op2ndg  7981  xpsneng  9026  xpcomeng  9033  sbth  9061  sbthfi  9163  unxpdom  9200  prcdnq  10946  mhmlem  18994  carsgmon  34305  brimageg  35915  brdomaing  35923  brrangeg  35924  rankung  36154  mbfresfi  37660  zindbi  42935  2sbc6g  44404  2sbc5g  44405  fmulcl  45579