Theorem rspc2va 3600

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 3599	. 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  3603  swopo  5557  f1ounsn  7247  soisores  7302  soisoi  7303  isocnv  7305  isotr  7311  ovrspc2v  7413  coof  7677  caofrss  7692  caonncan  7697  frpoins3xpg  8119  coflton  8635  wunpr  10662  injresinj  13749  seqcaopr2  14003  rlimcn3  15556  o1of2  15579  isprm6  16684  ssc2  17784  pospropd  18286  tleile  18380  mgmhmpropd  18625  mhmpropd  18719  grpidssd  18948  grpinvssd  18949  dfgrp3lem  18970  isnsg3  19092  cyccom  19135  symgextf1  19351  efgredlemd  19674  efgredlem  19677  rglcom4d  20120  rnghmmul  20358  domneq0  20617  issrngd  20764  lindfind  21725  lindsind  21726  mplsubglem  21908  mdetunilem1  22499  mdetunilem3  22501  mdetunilem4  22502  mdetunilem9  22507  decpmatmulsumfsupp  22660  pm2mpf1  22686  pm2mpmhmlem1  22705  t0sep  23211  tsmsxplem2  24041  comet  24401  nrmmetd  24462  tngngp  24542  reconnlem2  24716  iscmet3lem1  25191  iscmet3lem2  25192  dchrisumlem1  27400  pntpbnd1  27497  ssltsepc  27705  tgjustc1  28402  tgjustc2  28403  iscgrglt  28441  motcgr  28463  perpneq  28641  foot  28649  f1otrg  28798  axcontlem10  28900  frgr2wwlk1  30258  orngmul  33281  lindsunlem  33620  mndpluscn  33916  unelros  34161  difelros  34162  inelsros  34168  diffiunisros  34169  elmrsubrn  35507  ghomco  37885  sticksstones10  42143  sticksstones12a  42145  fsuppind  42578  mzpcl34  42719  ntrk0kbimka  44028  isotone1  44037  isotone2  44038  nnfoctbdjlem  46453  2arymaptf1  48642