Theorem rspc2va 3576

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052

This theorem is referenced by:  rspc2dv  3579  swopo  5550  f1ounsn  7227  soisores  7282  soisoi  7283  isocnv  7285  isotr  7291  ovrspc2v  7393  coof  7655  caofrss  7670  caonncan  7675  frpoins3xpg  8090  coflton  8607  wunpr  10632  injresinj  13746  seqcaopr2  14000  rlimcn3  15552  o1of2  15575  isprm6  16684  ssc2  17789  pospropd  18291  tleile  18385  mgmhmpropd  18666  mhmpropd  18760  grpidssd  18992  grpinvssd  18993  dfgrp3lem  19014  isnsg3  19135  cyccom  19178  symgextf1  19396  efgredlemd  19719  efgredlem  19722  rglcom4d  20192  rnghmmul  20429  domneq0  20685  issrngd  20832  orngmul  20842  lindfind  21796  lindsind  21797  mplsubglem  21977  mdetunilem1  22577  mdetunilem3  22579  mdetunilem4  22580  mdetunilem9  22585  decpmatmulsumfsupp  22738  pm2mpf1  22764  pm2mpmhmlem1  22783  t0sep  23289  tsmsxplem2  24119  comet  24478  nrmmetd  24539  tngngp  24619  reconnlem2  24793  iscmet3lem1  25258  iscmet3lem2  25259  dchrisumlem1  27452  pntpbnd1  27549  sltssepc  27763  tgjustc1  28543  tgjustc2  28544  iscgrglt  28582  motcgr  28604  perpneq  28782  foot  28790  f1otrg  28939  axcontlem10  29042  frgr2wwlk1  30399  lindsunlem  33768  mndpluscn  34070  unelros  34315  difelros  34316  inelsros  34322  diffiunisros  34323  elmrsubrn  35702  ghomco  38212  sticksstones10  42594  sticksstones12a  42596  fsuppind  43023  mzpcl34  43163  ntrk0kbimka  44466  isotone1  44475  isotone2  44476  nnfoctbdjlem  46883  2arymaptf1  49129