Theorem rspc2v 2894

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1373   ∈ wcel 2177  ∀wral 2485

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-v 2775

This theorem is referenced by:  rspc2va  2895  rspc3v  2897  disji2  4046  ontriexmidim  4583  wetriext  4638  f1veqaeq  5856  isorel  5895  oveqrspc2v  5989  fovcld  6068  caovclg  6117  caovcomg  6120  smoel  6404  dcdifsnid  6608  unfiexmid  7036  prfidceq  7046  fiintim  7049  supmoti  7116  supsnti  7128  isotilem  7129  onntri35  7378  onntri45  7382  cauappcvgprlem1  7802  caucvgprlemnkj  7809  caucvgprlemnbj  7810  caucvgprprlemval  7831  ltordlem  8585  frecuzrdgrrn  10585  frec2uzrdg  10586  frecuzrdgrcl  10587  frecuzrdgrclt  10592  seq3caopr3  10668  seq3homo  10704  seqhomog  10707  climcn2  11705  fprodcl2lem  12001  ennnfonelemim  12880  mhmlin  13384  issubg2m  13610  nsgbi  13625  ghmlin  13669  issubrng2  14057  issubrg2  14088  lmodlema  14139  islmodd  14140  rmodislmodlem  14197  rmodislmod  14198  rnglidlmcl  14327  inopn  14560  basis1  14604  basis2  14605  xmeteq0  14916  cncfi  15135  limccnp2lem  15233  logltb  15431  2sqlem8  15685  redcwlpo  16166  redc0  16168  reap0  16169