Theorem rspc2v 2877

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 2875	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  2878  rspc3v  2880  disji2  4022  ontriexmidim  4554  wetriext  4609  f1veqaeq  5812  isorel  5851  oveqrspc2v  5945  fovcld  6023  caovclg  6071  caovcomg  6074  smoel  6353  dcdifsnid  6557  unfiexmid  6974  fiintim  6985  supmoti  7052  supsnti  7064  isotilem  7065  onntri35  7297  onntri45  7301  cauappcvgprlem1  7719  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprprlemval  7748  ltordlem  8501  frecuzrdgrrn  10479  frec2uzrdg  10480  frecuzrdgrcl  10481  frecuzrdgrclt  10486  seq3caopr3  10562  seq3homo  10598  seqhomog  10601  climcn2  11452  fprodcl2lem  11748  ennnfonelemim  12581  mhmlin  13039  issubg2m  13259  nsgbi  13274  ghmlin  13318  issubrng2  13706  issubrg2  13737  lmodlema  13788  islmodd  13789  rmodislmodlem  13846  rmodislmod  13847  rnglidlmcl  13976  inopn  14171  basis1  14215  basis2  14216  xmeteq0  14527  cncfi  14733  limccnp2lem  14830  logltb  15009  2sqlem8  15210  redcwlpo  15545  redc0  15547  reap0  15548