Theorem rspc2v 3293

Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.)

Hypotheses

Ref	Expression
rspc2v.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
rspc2v.2	⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))

Assertion

Ref	Expression
rspc2v	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶   𝑥,𝐷,𝑦   𝜒,𝑥   𝜓,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥)   𝜒(𝑦)   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem rspc2v

Step	Hyp	Ref	Expression
1		nfv 1830	. 2 ⊢ Ⅎ𝑥𝜒
2		nfv 1830	. 2 ⊢ Ⅎ𝑦𝜓
3		rspc2v.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
4		rspc2v.2	. 2 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
5	1, 2, 3, 4	rspc2 3292	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175

This theorem is referenced by:  rspc2va  3294  rspc3v  3296  disji2  4569  f1veqaeq  6418  isorel  6476  isosolem  6497  oveqrspc2v  6572  fovcl  6663  caovclg  6724  caovcomg  6727  smoel  7344  fiint  8122  dffi3  8220  ltordlem  10432  seqhomo  12710  cshf1  13407  climcn2  14171  drsdir  16758  tsrlin  17042  dirge  17060  mhmlin  17165  issubg2  17432  nsgbi  17448  ghmlin  17488  efgi  17955  efgred  17984  irredmul  18532  issubrg2  18623  abvmul  18652  abvtri  18653  lmodlema  18691  islmodd  18692  lmhmlin  18856  lbsind  18901  mplcoe5lem  19288  ipcj  19798  obsip  19884  matecl  20050  dmatelnd  20121  scmateALT  20137  mdetdiaglem  20223  mdetdiagid  20225  pmatcoe1fsupp  20325  m2cpminvid2lem  20378  inopn  20529  basis1  20565  basis2  20566  iscldtop  20709  hausnei  20942  t1sep2  20983  nconsubb  21036  r0sep  21361  fbasssin  21450  fcfneii  21651  ustssel  21819  xmeteq0  21953  tngngp3  22270  nmvs  22290  cncfi  22505  c1lip1  23564  aalioulem3  23893  logltb  24150  cvxcl  24511  2sqlem8  24951  axtgcgrrflx  25161  axtgsegcon  25163  axtg5seg  25164  axtgbtwnid  25165  axtgpasch  25166  axtgcont1  25167  axtgupdim2  25170  axtgeucl  25171  iscgrglt  25209  isperp2d  25411  f1otrgds  25549  brbtwn2  25585  axcontlem3  25646  axcontlem9  25652  axcontlem10  25653  fargshiftf1  26165  ablocom  26786  nvs  26902  nvtri  26909  phpar2  27062  phpar  27063  shaddcl  27458  shmulcl  27459  cnopc  28156  unop  28158  hmop  28165  cnfnc  28173  adj1  28176  hstel2  28462  stj  28478  stcltr1i  28517  mddmdin0i  28674  cdj3lem1  28677  cdj3lem2b  28680  disji2f  28772  disjif2  28776  disjxpin  28783  fovcld  28820  isoun  28862  archirng  29073  archiexdiv  29075  slmdlema  29087  inelcarsg  29700  sibfof  29729  axtgupdim2OLD  29999  pconcn  30460  nocvxminlem  31089  nofulllem5  31105  ivthALT  31500  poimirlem32  32611  ismtycnv  32771  ismtyima  32772  ismtyres  32777  bfplem1  32791  bfplem2  32792  ghomlinOLD  32857  rngohomadd  32938  rngohommul  32939  crngocom  32970  idladdcl  32988  idllmulcl  32989  idlrmulcl  32990  pridl  33006  ispridlc  33039  pridlc  33040  dmnnzd  33044  oposlem  33487  omllaw  33548  hlsuprexch  33685  lautle  34388  ltrnu  34425  tendovalco  35071  ntrkbimka  37356  mullimc  38683  mullimcf  38690  lptre2pt  38707  fourierdlem54  39053  faovcl  39929  icceuelpartlem  39973  iccpartnel  39976  upgrwlkdvdelem  40942  conngrv2edg  41362  frgr2wwlkeqm  41496  mgmhmlin  41576  issubmgm2  41580