Theorem rspc2va 3633

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059

This theorem is referenced by:  rspc2dv  3636  swopo  5607  f1ounsn  7291  soisores  7346  soisoi  7347  isocnv  7349  isotr  7355  ovrspc2v  7456  coof  7720  caofrss  7734  caonncan  7739  frpoins3xpg  8163  coflton  8707  wunpr  10746  injresinj  13823  seqcaopr2  14075  rlimcn3  15622  o1of2  15645  isprm6  16747  ssc2  17869  pospropd  18384  tleile  18478  mgmhmpropd  18723  mhmpropd  18817  grpidssd  19046  grpinvssd  19047  dfgrp3lem  19068  isnsg3  19190  cyccom  19233  symgextf1  19453  efgredlemd  19776  efgredlem  19779  rglcom4d  20228  rnghmmul  20465  domneq0  20724  issrngd  20872  lindfind  21853  lindsind  21854  mplsubglem  22036  mdetunilem1  22633  mdetunilem3  22635  mdetunilem4  22636  mdetunilem9  22641  decpmatmulsumfsupp  22794  pm2mpf1  22820  pm2mpmhmlem1  22839  t0sep  23347  tsmsxplem2  24177  comet  24541  nrmmetd  24602  tngngp  24690  reconnlem2  24862  iscmet3lem1  25338  iscmet3lem2  25339  dchrisumlem1  27547  pntpbnd1  27644  ssltsepc  27852  tgjustc1  28497  tgjustc2  28498  iscgrglt  28536  motcgr  28558  perpneq  28736  foot  28744  f1otrg  28893  axcontlem10  29002  frgr2wwlk1  30357  orngmul  33312  lindsunlem  33651  mndpluscn  33886  unelros  34151  difelros  34152  inelsros  34158  diffiunisros  34159  elmrsubrn  35504  ghomco  37877  sticksstones10  42136  sticksstones12a  42138  fsuppind  42576  mzpcl34  42718  ntrk0kbimka  44028  isotone1  44037  isotone2  44038  nnfoctbdjlem  46410  2arymaptf1  48502