Theorem vtocl2g 3540

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.) Remove dependency on ax-10 2179, ax-11 2195, and ax-13 2406. (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 3478	. 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 3524	. . 3 ⊢ (𝐴 ∈ V → 𝜓)
7	3, 6	vtoclg 3524	. 2 ⊢ (𝐵 ∈ 𝑊 → (𝐴 ∈ V → 𝜒))
8	1, 7	mpan9 516	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒)

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459

This theorem is used by:  vtocl3g  3541  vtocl4g  3548  opthg  5461  opelopabsb  5516  vtoclr  5726  funopg  6574  f1osng  6867  fsng  7137  fnpr2g  7215  op1stg  8004  op2ndg  8005  xpsneng  9057  xpcomeng  9064  sbth  9092  sbthfi  9190  unxpdom  9226  prcdnq  10993  mhmlem  19172  carsgmon  34769  brimageg  36454  brdomaing  36462  brrangeg  36463  rankung  36695  mbfresfi  38374  zindbi  43731  2sbc6g  45183  2sbc5g  45184  fmulcl  46355