Theorem rspc2v 2934

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1398   ∈ wcel 2203  ∀wral 2520

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-v 2815

This theorem is referenced by:  rspc2va  2935  rspc3v  2937  disji2  4101  ontriexmidim  4644  wetriext  4699  f1veqaeq  5942  isorel  5981  oveqrspc2v  6077  fovcld  6158  caovclg  6207  caovcomg  6210  smoel  6531  dcdifsnid  6737  unfiexmid  7178  prfidceq  7188  fiintim  7191  supmoti  7284  supsnti  7296  isotilem  7297  onntri35  7547  onntri45  7551  cauappcvgprlem1  7974  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprprlemval  8003  ltordlem  8756  frecuzrdgrrn  10770  frec2uzrdg  10771  frecuzrdgrcl  10772  frecuzrdgrclt  10777  seq3caopr3  10853  seq3homo  10889  seqhomog  10892  climcn2  11994  fprodcl2lem  12291  ennnfonelemim  13175  mhmlin  13680  issubg2m  13906  nsgbi  13921  ghmlin  13965  issubrng2  14355  issubrg2  14386  lmodlema  14440  islmodd  14441  rmodislmodlem  14498  rmodislmod  14499  rnglidlmcl  14628  inopn  14868  basis1  14912  basis2  14913  xmeteq0  15224  cncfi  15443  limccnp2lem  15541  logltb  15739  2sqlem8  15996  redcwlpo  16840  redc0  16842  reap0  16843