Theorem rspc2va 3594

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1561   ∈ wcel 2143  ∀wral 3077

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3078

This theorem is referenced by:  rspc2dv  3597  swopo  5567  f1ounsn  7257  soisores  7312  soisoi  7313  isocnv  7315  isotr  7321  ovrspc2v  7423  coof  7685  caofrss  7700  caonncan  7705  frpoins3xpg  8121  coflton  8642  wunpr  10668  injresinj  13798  seqcaopr2  14052  rlimcn3  15618  o1of2  15641  isprm6  16750  ssc2  17856  pospropd  18358  tleile  18452  mgmhmpropd  18733  mhmpropd  18827  grpidssd  19059  grpinvssd  19060  dfgrp3lem  19081  isnsg3  19202  cyccom  19245  symgextf1  19462  efgredlemd  19785  efgredlem  19788  rglcom4d  20262  rnghmmul  20499  domneq0  20759  issrngd  20905  orngmul  20915  lindfind  21869  lindsind  21870  mplsubglem  22051  mdetunilem1  22673  mdetunilem3  22675  mdetunilem4  22676  mdetunilem9  22681  decpmatmulsumfsupp  22834  pm2mpf1  22860  pm2mpmhmlem1  22879  t0sep  23385  tsmsxplem2  24215  comet  24574  nrmmetd  24635  tngngp  24715  reconnlem2  24889  iscmet3lem1  25354  iscmet3lem2  25355  dchrisumlem1  27554  pntpbnd1  27651  sltssepc  27865  tgjustc1  28645  tgjustc2  28646  iscgrglt  28684  motcgr  28706  perpneq  28888  foot  28896  f1otrg  29072  axcontlem10  29175  frgr2wwlk1  30532  lindsunlem  33922  mndpluscn  34224  unelros  34469  difelros  34470  inelsros  34476  diffiunisros  34477  elmrsubrn  35871  ghomco  38391  sticksstones10  42773  sticksstones12a  42775  fsuppind  43173  mzpcl34  43313  ntrk0kbimka  44616  isotone1  44625  isotone2  44626  nnfoctbdjlem  47030  2arymaptf1  49276