Theorem vtocl2g 3534

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453

This theorem is used by:  vtocl3g  3535  vtocl4g  3542  opthg  5446  opelopabsb  5504  vtoclr  5714  funopg  6572  f1osng  6865  fsng  7136  fnpr2g  7214  op1stg  8011  op2ndg  8012  xpsneng  9074  xpcomeng  9081  sbth  9109  sbthfi  9207  unxpdom  9243  rankung  9866  prcdnq  11071  mhmlem  19265  carsgmon  34939  brimageg  36669  brdomaing  36677  brrangeg  36678  mbfresfi  38564  zindbi  43932  2sbc6g  45384  2sbc5g  45385  fmulcl  46562