Theorem rspc2va 3563

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068

This theorem is referenced by:  swopo  5505  soisores  7178  soisoi  7179  isocnv  7181  isotr  7187  ovrspc2v  7281  caofrss  7547  caonncan  7552  wunpr  10396  injresinj  13436  seqcaopr2  13687  rlimcn3  15227  o1of2  15250  isprm6  16347  ssc2  17451  pospropd  17960  tleile  18054  mhmpropd  18351  grpidssd  18566  grpinvssd  18567  dfgrp3lem  18588  isnsg3  18703  cyccom  18737  symgextf1  18944  efgredlemd  19265  efgredlem  19268  issrngd  20036  domneq0  20481  lindfind  20933  lindsind  20934  mplsubglem  21115  mdetunilem1  21669  mdetunilem3  21671  mdetunilem4  21672  mdetunilem9  21677  decpmatmulsumfsupp  21830  pm2mpf1  21856  pm2mpmhmlem1  21875  t0sep  22383  tsmsxplem2  23213  comet  23575  nrmmetd  23636  tngngp  23724  reconnlem2  23896  iscmet3lem1  24360  iscmet3lem2  24361  dchrisumlem1  26542  pntpbnd1  26639  tgjustc1  26740  tgjustc2  26741  iscgrglt  26779  motcgr  26801  perpneq  26979  foot  26987  f1otrg  27136  axcontlem10  27244  frgr2wwlk1  28594  orngmul  31404  lindsunlem  31607  mndpluscn  31778  unelros  32039  difelros  32040  inelsros  32046  diffiunisros  32047  cvxsconn  33105  elmrsubrn  33382  frpoins3xpg  33714  ssltsepc  33914  ghomco  35976  sticksstones10  40039  sticksstones12a  40041  fsuppind  40202  mzpcl34  40469  ntrk0kbimka  41538  isotone1  41547  isotone2  41548  nnfoctbdjlem  43883  isomuspgrlem2d  45171  mgmhmpropd  45227  rnghmmul  45346  2arymaptf1  45887