MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vtocl2ga Structured version   Visualization version   GIF version

Theorem vtocl2ga 3578
Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2141 and ax-11 2157. (Revised by GG, 20-Aug-2023.) (Proof shortened by Wolf Lammen, 23-Aug-2023.)
Hypotheses
Ref Expression
vtocl2ga.1 (𝑥 = 𝐴 → (𝜑𝜓))
vtocl2ga.2 (𝑦 = 𝐵 → (𝜓𝜒))
vtocl2ga.3 ((𝑥𝐶𝑦𝐷) → 𝜑)
Assertion
Ref Expression
vtocl2ga ((𝐴𝐶𝐵𝐷) → 𝜒)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝜓,𝑥   𝜒,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)   𝜒(𝑥)   𝐵(𝑥)

Proof of Theorem vtocl2ga
StepHypRef Expression
1 vtocl2ga.2 . . . 4 (𝑦 = 𝐵 → (𝜓𝜒))
21imbi2d 340 . . 3 (𝑦 = 𝐵 → ((𝐴𝐶𝜓) ↔ (𝐴𝐶𝜒)))
3 vtocl2ga.1 . . . . . 6 (𝑥 = 𝐴 → (𝜑𝜓))
43imbi2d 340 . . . . 5 (𝑥 = 𝐴 → ((𝑦𝐷𝜑) ↔ (𝑦𝐷𝜓)))
5 vtocl2ga.3 . . . . . 6 ((𝑥𝐶𝑦𝐷) → 𝜑)
65ex 412 . . . . 5 (𝑥𝐶 → (𝑦𝐷𝜑))
74, 6vtoclga 3577 . . . 4 (𝐴𝐶 → (𝑦𝐷𝜓))
87com12 32 . . 3 (𝑦𝐷 → (𝐴𝐶𝜓))
92, 8vtoclga 3577 . 2 (𝐵𝐷 → (𝐴𝐶𝜒))
109impcom 407 1 ((𝐴𝐶𝐵𝐷) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108
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 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816
This theorem is referenced by:  vtocl3ga  3583  vtocl4ga  3586  solin  5619  caovcan  7637  xpord2pred  8170  pwfseqlem2  10699  mulcanenq  11000  ltaddnq  11014  ltrnq  11019  genpv  11039  wrdind  14760  fsumrelem  15843  imasleval  17586  fullfunc  17953  fthfunc  17954  symggrplem  18897  pf1ind  22359  mretopd  23100  dvlip  26032  scvxcvx  27029  issubgoilem  31279  cnre2csqlem  33909
  Copyright terms: Public domain W3C validator