Theorem rcla42v 1927

Description: 2-variable restricted specialization, using implicit substitition.

Hypotheses

Ref	Expression
rcla42v.1	⊢ (x = A → (φ ↔ χ))
rcla42v.2	⊢ (y = B → (χ ↔ ψ))

Assertion

Ref	Expression
rcla42v	⊢ ((A ∈ C ⋀ B ∈ D) → (∀x ∈ C ∀y ∈ D φ → ψ))

Distinct variable groups:   x,y,A   x,C   x,D   y,B   y,D   χ,x   ψ,y

Proof of Theorem rcla42v

Step	Hyp	Ref	Expression
1		rcla42v.1	. . . 4 ⊢ (x = A → (φ ↔ χ))
2	1	ralbidv 1710	. . 3 ⊢ (x = A → (∀y ∈ D φ ↔ ∀y ∈ D χ))
3	2	rcla4v 1920	. 2 ⊢ (A ∈ C → (∀x ∈ C ∀y ∈ D φ → ∀y ∈ D χ))
4		rcla42v.2	. . 3 ⊢ (y = B → (χ ↔ ψ))
5	4	rcla4v 1920	. 2 ⊢ (B ∈ D → (∀y ∈ D χ → ψ))
6	3, 5	sylan9 479	1 ⊢ ((A ∈ C ⋀ B ∈ D) → (∀x ∈ C ∀y ∈ D φ → ψ))

Syntax hints:   → wi 3   ↔ wb 153   ⋀ wa 230   = wceq 997   ∈ wcel 999  ∀wral 1692

This theorem is referenced by:  rcla43v 1929  isorel 3952  isocnv 3954  isotr 3955  isotrALT 3956  foprcl 4073  fiint 4620  seq1rn2 6580  seqzrn2 6645  infxpidmlem7 7650  inopn 7691  basis1 7703  basis2 7704  tgss2 7726  hausnei 7869  meteq0 7897  metcni 7979  ablcom 8187  ghgrpilem1 8217  nvs 8374  nvtri 8382  phpar2 8566  phpar 8567  logltb 8859  shaddcl 9168  shaddclOLD 9169  shmulcl 9170  shmulclOLD 9171  unop 9922  hmop 9929  adj1 9940  hstel2 10230  stj 10246  stcltr1i 10285  mddmdin0i 10442  cdj3lem1 10445  cdj3lem2b 10448  ghomlin 10478  ghomf1olem 10481  filint 10656  cmppfd 10760  domcmpd 10761  codcmpd 10762  cmpida 10789  cmpidb 10790  ismonb2 10822  cmpmon 10825  isepib2 10832

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518  df-ral 1696  df-v 1859

Copyright terms: Public domain