Theorem rspc2v 2923

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1397   ∈ wcel 2202  ∀wral 2510

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804

This theorem is referenced by:  rspc2va  2924  rspc3v  2926  disji2  4080  ontriexmidim  4620  wetriext  4675  f1veqaeq  5910  isorel  5949  oveqrspc2v  6045  fovcld  6126  caovclg  6175  caovcomg  6178  smoel  6466  dcdifsnid  6672  unfiexmid  7110  prfidceq  7120  fiintim  7123  supmoti  7192  supsnti  7204  isotilem  7205  onntri35  7455  onntri45  7459  cauappcvgprlem1  7879  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprprlemval  7908  ltordlem  8662  frecuzrdgrrn  10671  frec2uzrdg  10672  frecuzrdgrcl  10673  frecuzrdgrclt  10678  seq3caopr3  10754  seq3homo  10790  seqhomog  10793  climcn2  11887  fprodcl2lem  12184  ennnfonelemim  13063  mhmlin  13568  issubg2m  13794  nsgbi  13809  ghmlin  13853  issubrng2  14243  issubrg2  14274  lmodlema  14325  islmodd  14326  rmodislmodlem  14383  rmodislmod  14384  rnglidlmcl  14513  inopn  14746  basis1  14790  basis2  14791  xmeteq0  15102  cncfi  15321  limccnp2lem  15419  logltb  15617  2sqlem8  15871  redcwlpo  16711  redc0  16713  reap0  16714