Theorem rspc2v 2878

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1364   ∈ wcel 2164  ∀wral 2472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-v 2762

This theorem is referenced by:  rspc2va  2879  rspc3v  2881  disji2  4023  ontriexmidim  4555  wetriext  4610  f1veqaeq  5813  isorel  5852  oveqrspc2v  5946  fovcld  6024  caovclg  6073  caovcomg  6076  smoel  6355  dcdifsnid  6559  unfiexmid  6976  fiintim  6987  supmoti  7054  supsnti  7066  isotilem  7067  onntri35  7299  onntri45  7303  cauappcvgprlem1  7721  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprprlemval  7750  ltordlem  8503  frecuzrdgrrn  10482  frec2uzrdg  10483  frecuzrdgrcl  10484  frecuzrdgrclt  10489  seq3caopr3  10565  seq3homo  10601  seqhomog  10604  climcn2  11455  fprodcl2lem  11751  ennnfonelemim  12584  mhmlin  13042  issubg2m  13262  nsgbi  13277  ghmlin  13321  issubrng2  13709  issubrg2  13740  lmodlema  13791  islmodd  13792  rmodislmodlem  13849  rmodislmod  13850  rnglidlmcl  13979  inopn  14182  basis1  14226  basis2  14227  xmeteq0  14538  cncfi  14757  limccnp2lem  14855  logltb  15050  2sqlem8  15280  redcwlpo  15615  redc0  15617  reap0  15618