Theorem rspc2va 3591

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2146  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081

This theorem is used by:  rspc2dv  3594  swopo  5574  f1ounsn  7290  soisores  7345  soisoi  7346  isocnv  7348  isotr  7354  ovrspc2v  7456  coof  7727  caofrss  7742  caonncan  7747  frpoins3xpg  8170  coflton  8694  wunpr  10807  injresinj  13939  seqcaopr2  14194  rlimcn3  15772  o1of2  15795  isprm6  16905  ssc2  18012  pospropd  18514  tleile  18608  mgmhmpropd  18902  mhmpropd  19002  grpidssd  19241  grpinvssd  19242  dfgrp3lem  19263  isnsg3  19385  cyccom  19433  symgextf1  19650  efgredlemd  19973  efgredlem  19976  rglcom4d  20452  rnghmmul  20694  domneq0  20975  issrngd  21127  orngmul  21137  lindfind  22137  lindsind  22138  mplsubglem  22321  mdetunilem1  22942  mdetunilem3  22944  mdetunilem4  22945  mdetunilem9  22950  decpmatmulsumfsupp  23106  pm2mpf1  23132  pm2mpmhmlem1  23151  t0sep  23657  tsmsxplem2  24488  comet  24847  nrmmetd  24908  tngngp  24988  reconnlem2  25162  iscmet3lem1  25627  iscmet3lem2  25628  dchrisumlem1  27831  pntpbnd1  27928  sltssepc  28172  tgjustc1  28952  tgjustc2  28953  iscgrglt  28992  motcgr  29014  perpneq  29204  foot  29212  f1otrg  29463  axcontlem10  29566  frgr2wwlk1  30945  lindsunlem  34312  mndpluscn  34614  unelros  34860  difelros  34861  inelsros  34867  diffiunisros  34868  elmrsubrn  36409  nmuladdel  37091  ghomco  38968  sticksstones10  43348  sticksstones12a  43350  fsuppind  43761  mzpcl34  43885  ntrk0kbimka  45182  isotone1  45191  isotone2  45192  nnfoctbdjlem  47607  2arymaptf1  49907