Theorem rspc2va 3294

Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 18-Jun-2014.)

Hypotheses

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

Assertion

Ref	Expression
rspc2va	⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓)

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

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

Proof of Theorem rspc2va

Step	Hyp	Ref	Expression
1		rspc2v.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2		rspc2v.2	. . 3 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
3	1, 2	rspc2v 3293	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))
4	3	imp 444	1 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175

This theorem is referenced by:  swopo  4969  soisores  6477  soisoi  6478  isocnv  6480  isotr  6486  ovrspc2v  6571  off  6810  caofrss  6828  caonncan  6833  wunpr  9410  injresinj  12451  seqcaopr2  12699  rlimcn2  14169  o1of2  14191  isprm6  15264  ssc2  16305  pospropd  16957  mhmpropd  17164  grpidssd  17314  grpinvssd  17315  dfgrp3lem  17336  isnsg3  17451  symgextf1  17664  efgredlemd  17980  efgredlem  17983  issrngd  18684  domneq0  19118  mplsubglem  19255  lindfind  19974  lindsind  19975  mdetunilem1  20237  mdetunilem3  20239  mdetunilem4  20240  mdetunilem9  20245  decpmatmulsumfsupp  20397  pm2mpf1  20423  pm2mpmhmlem1  20442  t0sep  20938  tsmsxplem2  21767  comet  22128  nrmmetd  22189  tngngp  22268  reconnlem2  22438  iscmet3lem1  22897  iscmet3lem2  22898  dchrisumlem1  24978  pntpbnd1  25075  motcgr  25231  perpneq  25409  foot  25414  f1otrg  25551  axcontlem10  25653  frg2wot1  26584  tleile  28992  orngmul  29134  mndpluscn  29300  unelros  29561  difelros  29562  inelsros  29568  diffiunisros  29569  cvxscon  30479  elmrsubrn  30671  ghomco  32860  mzpcl34  36312  ntrk0kbimka  37357  isotone1  37366  isotone2  37367  nnfoctbdjlem  39348  frgr2wwlk1  41494  mgmhmpropd  41575  rnghmmul  41690