Theorem rspc2va 3624

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063

This theorem is referenced by:  rspc2dv  3627  swopo  5600  soisores  7324  soisoi  7325  isocnv  7327  isotr  7333  ovrspc2v  7435  caofrss  7706  caonncan  7711  frpoins3xpg  8126  coflton  8670  wunpr  10704  injresinj  13753  seqcaopr2  14004  rlimcn3  15534  o1of2  15557  isprm6  16651  ssc2  17769  pospropd  18280  tleile  18374  mhmpropd  18678  grpidssd  18899  grpinvssd  18900  dfgrp3lem  18921  isnsg3  19040  cyccom  19080  symgextf1  19289  efgredlemd  19612  efgredlem  19615  rglcom4d  20034  issrngd  20469  domneq0  20913  lindfind  21371  lindsind  21372  mplsubglem  21558  mdetunilem1  22114  mdetunilem3  22116  mdetunilem4  22117  mdetunilem9  22122  decpmatmulsumfsupp  22275  pm2mpf1  22301  pm2mpmhmlem1  22320  t0sep  22828  tsmsxplem2  23658  comet  24022  nrmmetd  24083  tngngp  24171  reconnlem2  24343  iscmet3lem1  24808  iscmet3lem2  24809  dchrisumlem1  26992  pntpbnd1  27089  ssltsepc  27295  tgjustc1  27757  tgjustc2  27758  iscgrglt  27796  motcgr  27818  perpneq  27996  foot  28004  f1otrg  28153  axcontlem10  28262  frgr2wwlk1  29613  orngmul  32452  lindsunlem  32740  mndpluscn  32937  unelros  33200  difelros  33201  inelsros  33207  diffiunisros  33208  cvxsconn  34265  elmrsubrn  34542  ghomco  36807  sticksstones10  41019  sticksstones12a  41021  fsuppind  41210  mzpcl34  41517  ntrk0kbimka  42838  isotone1  42847  isotone2  42848  nnfoctbdjlem  45219  isomuspgrlem2d  46547  mgmhmpropd  46603  rnghmmul  46746  2arymaptf1  47387