Theorem rspc2va 3584

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048

This theorem is referenced by:  rspc2dv  3587  swopo  5533  f1ounsn  7206  soisores  7261  soisoi  7262  isocnv  7264  isotr  7270  ovrspc2v  7372  coof  7634  caofrss  7649  caonncan  7654  frpoins3xpg  8070  coflton  8586  wunpr  10600  injresinj  13691  seqcaopr2  13945  rlimcn3  15497  o1of2  15520  isprm6  16625  ssc2  17729  pospropd  18231  tleile  18325  mgmhmpropd  18606  mhmpropd  18700  grpidssd  18929  grpinvssd  18930  dfgrp3lem  18951  isnsg3  19072  cyccom  19115  symgextf1  19333  efgredlemd  19656  efgredlem  19659  rglcom4d  20129  rnghmmul  20367  domneq0  20623  issrngd  20770  orngmul  20780  lindfind  21753  lindsind  21754  mplsubglem  21936  mdetunilem1  22527  mdetunilem3  22529  mdetunilem4  22530  mdetunilem9  22535  decpmatmulsumfsupp  22688  pm2mpf1  22714  pm2mpmhmlem1  22733  t0sep  23239  tsmsxplem2  24069  comet  24428  nrmmetd  24489  tngngp  24569  reconnlem2  24743  iscmet3lem1  25218  iscmet3lem2  25219  dchrisumlem1  27427  pntpbnd1  27524  ssltsepc  27734  tgjustc1  28453  tgjustc2  28454  iscgrglt  28492  motcgr  28514  perpneq  28692  foot  28700  f1otrg  28849  axcontlem10  28951  frgr2wwlk1  30309  lindsunlem  33637  mndpluscn  33939  unelros  34184  difelros  34185  inelsros  34191  diffiunisros  34192  elmrsubrn  35564  ghomco  37941  sticksstones10  42258  sticksstones12a  42260  fsuppind  42693  mzpcl34  42834  ntrk0kbimka  44142  isotone1  44151  isotone2  44152  nnfoctbdjlem  46563  2arymaptf1  48764