Theorem rspc2va 3597

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  rspc2dv  3600  swopo  5550  f1ounsn  7229  soisores  7284  soisoi  7285  isocnv  7287  isotr  7293  ovrspc2v  7395  coof  7657  caofrss  7672  caonncan  7677  frpoins3xpg  8096  coflton  8612  wunpr  10638  injresinj  13725  seqcaopr2  13979  rlimcn3  15532  o1of2  15555  isprm6  16660  ssc2  17764  pospropd  18266  tleile  18360  mgmhmpropd  18607  mhmpropd  18701  grpidssd  18930  grpinvssd  18931  dfgrp3lem  18952  isnsg3  19074  cyccom  19117  symgextf1  19335  efgredlemd  19658  efgredlem  19661  rglcom4d  20131  rnghmmul  20369  domneq0  20628  issrngd  20775  orngmul  20785  lindfind  21758  lindsind  21759  mplsubglem  21941  mdetunilem1  22532  mdetunilem3  22534  mdetunilem4  22535  mdetunilem9  22540  decpmatmulsumfsupp  22693  pm2mpf1  22719  pm2mpmhmlem1  22738  t0sep  23244  tsmsxplem2  24074  comet  24434  nrmmetd  24495  tngngp  24575  reconnlem2  24749  iscmet3lem1  25224  iscmet3lem2  25225  dchrisumlem1  27433  pntpbnd1  27530  ssltsepc  27739  tgjustc1  28455  tgjustc2  28456  iscgrglt  28494  motcgr  28516  perpneq  28694  foot  28702  f1otrg  28851  axcontlem10  28953  frgr2wwlk1  30308  lindsunlem  33613  mndpluscn  33909  unelros  34154  difelros  34155  inelsros  34161  diffiunisros  34162  elmrsubrn  35500  ghomco  37878  sticksstones10  42136  sticksstones12a  42138  fsuppind  42571  mzpcl34  42712  ntrk0kbimka  44021  isotone1  44030  isotone2  44031  nnfoctbdjlem  46446  2arymaptf1  48635