Theorem rspc2va 3634

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062

This theorem is referenced by:  rspc2dv  3637  swopo  5603  f1ounsn  7292  soisores  7347  soisoi  7348  isocnv  7350  isotr  7356  ovrspc2v  7457  coof  7721  caofrss  7736  caonncan  7741  frpoins3xpg  8165  coflton  8709  wunpr  10749  injresinj  13827  seqcaopr2  14079  rlimcn3  15626  o1of2  15649  isprm6  16751  ssc2  17866  pospropd  18372  tleile  18466  mgmhmpropd  18711  mhmpropd  18805  grpidssd  19034  grpinvssd  19035  dfgrp3lem  19056  isnsg3  19178  cyccom  19221  symgextf1  19439  efgredlemd  19762  efgredlem  19765  rglcom4d  20208  rnghmmul  20449  domneq0  20708  issrngd  20856  lindfind  21836  lindsind  21837  mplsubglem  22019  mdetunilem1  22618  mdetunilem3  22620  mdetunilem4  22621  mdetunilem9  22626  decpmatmulsumfsupp  22779  pm2mpf1  22805  pm2mpmhmlem1  22824  t0sep  23332  tsmsxplem2  24162  comet  24526  nrmmetd  24587  tngngp  24675  reconnlem2  24849  iscmet3lem1  25325  iscmet3lem2  25326  dchrisumlem1  27533  pntpbnd1  27630  ssltsepc  27838  tgjustc1  28483  tgjustc2  28484  iscgrglt  28522  motcgr  28544  perpneq  28722  foot  28730  f1otrg  28879  axcontlem10  28988  frgr2wwlk1  30348  orngmul  33333  lindsunlem  33675  mndpluscn  33925  unelros  34172  difelros  34173  inelsros  34179  diffiunisros  34180  elmrsubrn  35525  ghomco  37898  sticksstones10  42156  sticksstones12a  42158  fsuppind  42600  mzpcl34  42742  ntrk0kbimka  44052  isotone1  44061  isotone2  44062  nnfoctbdjlem  46470  2arymaptf1  48574