Theorem rspc2va 3590

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 3589	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))
4	3	imp 406	1 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053

This theorem is referenced by:  rspc2dv  3593  swopo  5551  f1ounsn  7228  soisores  7283  soisoi  7284  isocnv  7286  isotr  7292  ovrspc2v  7394  coof  7656  caofrss  7671  caonncan  7676  frpoins3xpg  8092  coflton  8609  wunpr  10632  injresinj  13719  seqcaopr2  13973  rlimcn3  15525  o1of2  15548  isprm6  16653  ssc2  17758  pospropd  18260  tleile  18354  mgmhmpropd  18635  mhmpropd  18729  grpidssd  18961  grpinvssd  18962  dfgrp3lem  18983  isnsg3  19104  cyccom  19147  symgextf1  19365  efgredlemd  19688  efgredlem  19691  rglcom4d  20161  rnghmmul  20400  domneq0  20656  issrngd  20803  orngmul  20813  lindfind  21786  lindsind  21787  mplsubglem  21969  mdetunilem1  22571  mdetunilem3  22573  mdetunilem4  22574  mdetunilem9  22579  decpmatmulsumfsupp  22732  pm2mpf1  22758  pm2mpmhmlem1  22777  t0sep  23283  tsmsxplem2  24113  comet  24472  nrmmetd  24533  tngngp  24613  reconnlem2  24787  iscmet3lem1  25262  iscmet3lem2  25263  dchrisumlem1  27471  pntpbnd1  27568  sltssepc  27782  tgjustc1  28563  tgjustc2  28564  iscgrglt  28602  motcgr  28624  perpneq  28802  foot  28810  f1otrg  28959  axcontlem10  29062  frgr2wwlk1  30420  lindsunlem  33806  mndpluscn  34108  unelros  34353  difelros  34354  inelsros  34360  diffiunisros  34361  elmrsubrn  35740  ghomco  38146  sticksstones10  42529  sticksstones12a  42531  fsuppind  42952  mzpcl34  43092  ntrk0kbimka  44399  isotone1  44408  isotone2  44409  nnfoctbdjlem  46817  2arymaptf1  49017