Theorem rspc2v 3353

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 1883	. 2 ⊢ Ⅎ𝑥𝜒
2		nfv 1883	. 2 ⊢ Ⅎ𝑦𝜓
3		rspc2v.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
4		rspc2v.2	. 2 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
5	1, 2, 3, 4	rspc2 3351	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523   ∈ wcel 2030  ∀wral 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-v 3233

This theorem is referenced by:  rspc2va  3354  rspc3v  3356  disji2  4668  f1veqaeq  6554  isorel  6616  isosolem  6637  oveqrspc2v  6713  fovcl  6807  caovclg  6868  caovcomg  6871  smoel  7502  fiint  8278  dffi3  8378  ltordlem  10591  seqhomo  12888  cshf1  13602  climcn2  14367  drsdir  16982  tsrlin  17266  dirge  17284  mhmlin  17389  issubg2  17656  nsgbi  17672  ghmlin  17712  efgi  18178  efgred  18207  irredmul  18755  issubrg2  18848  abvmul  18877  abvtri  18878  lmodlema  18916  islmodd  18917  rmodislmodlem  18978  rmodislmod  18979  lmhmlin  19083  lbsind  19128  mplcoe5lem  19515  ipcj  20027  obsip  20113  matecl  20279  dmatelnd  20350  scmateALT  20366  mdetdiaglem  20452  mdetdiagid  20454  pmatcoe1fsupp  20554  m2cpminvid2lem  20607  inopn  20752  basis1  20802  basis2  20803  iscldtop  20947  hausnei  21180  t1sep2  21221  nconnsubb  21274  r0sep  21599  fbasssin  21687  fcfneii  21888  ustssel  22056  xmeteq0  22190  tngngp3  22507  nmvs  22527  cncfi  22744  c1lip1  23805  aalioulem3  24134  logltb  24391  cvxcl  24756  2sqlem8  25196  axtgcgrrflx  25406  axtgsegcon  25408  axtg5seg  25409  axtgbtwnid  25410  axtgpasch  25411  axtgcont1  25412  axtgupdim2  25415  axtgeucl  25416  iscgrglt  25454  isperp2d  25656  f1otrgds  25794  brbtwn2  25830  axcontlem3  25891  axcontlem9  25897  axcontlem10  25898  upgrwlkdvdelem  26688  conngrv2edg  27173  frgrwopreglem5ALT  27302  ablocom  27530  nvs  27646  nvtri  27653  phpar2  27806  phpar  27807  shaddcl  28202  shmulcl  28203  cnopc  28900  unop  28902  hmop  28909  cnfnc  28917  adj1  28920  hstel2  29206  stj  29222  stcltr1i  29261  mddmdin0i  29418  cdj3lem1  29421  cdj3lem2b  29424  disji2f  29516  disjif2  29520  disjxpin  29527  fovcld  29568  isoun  29607  archirng  29870  archiexdiv  29872  slmdlema  29884  inelcarsg  30501  sibfof  30530  breprexplema  30836  axtgupdim2OLD  30874  pconncn  31332  nocvxminlem  32018  ivthALT  32455  poimirlem32  33571  ismtycnv  33731  ismtyima  33732  ismtyres  33737  bfplem1  33751  bfplem2  33752  ghomlinOLD  33817  rngohomadd  33898  rngohommul  33899  crngocom  33930  idladdcl  33948  idllmulcl  33949  idlrmulcl  33950  pridl  33966  ispridlc  33999  pridlc  34000  dmnnzd  34004  oposlem  34787  omllaw  34848  hlsuprexch  34985  lautle  35688  ltrnu  35725  tendovalco  36370  ntrkbimka  38653  mullimc  40166  mullimcf  40173  lptre2pt  40190  fourierdlem54  40695  faovcl  41601  icceuelpartlem  41696  iccpartnel  41699  fargshiftf1  41702  sprsymrelfolem2  42068  mgmhmlin  42111  issubmgm2  42115