Theorem 2ralbidva 3227

Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Dec-2019.)

Hypothesis

Ref	Expression
2ralbidva.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
2ralbidva	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Distinct variable groups:   𝑥,𝑦,𝜑   𝑦,𝐴

Allowed substitution hints:   𝜓(𝑥, 𝑦)   𝜒(𝑥, 𝑦)   𝐴(𝑥)   𝐵(𝑥, 𝑦)

Proof of Theorem 2ralbidva

Step	Hyp	Ref	Expression
1		2ralbidva.1	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒))
2	1	anassrs 472	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒))
3	2	ralbidva 3186	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
4	3	ralbidva 3186	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2143  ∀wral 3079

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This proof depends on definitions:  df-bi 210  df-an 401  df-ral 3080

This theorem is used by:  disjxun  5107  reu3op  6293  opreu2reurex  6295  isocnv3  7330  isotr  7334  f1oweALT  7965  fnmpoovd  8078  pospropd  18385  tosso  18477  isipodrs  18597  mgmpropd  18713  mgmhmpropd  18760  sgrppropd  18793  mndpropd  18821  mhmpropd  18854  efgred  19822  cmnpropd  19865  rngpropd  20256  ringpropd  20376  isdomn3  20822  lmodprop2d  21054  lsspropd  21147  islmhm2  21168  lmhmpropd  21203  df2idl2crng  21430  islindf4  21997  assapropd  22030  scmatmats  22677  cpmatel2  22879  1elcpmat  22881  m2cpminvid2  22921  decpmataa0  22934  pmatcollpw2lem  22943  connsub  23587  hausdiag  23811  ist0-4  23895  ismet2  24499  txmetcnp  24713  txmetcn  24714  metuel2  24731  metucn  24737  isngp3  24764  nlmvscn  24853  isclmp  25265  isncvsngp  25317  ipcn  25414  iscfil2  25434  caucfil  25451  cfilresi  25463  ulmdvlem3  26574  cxpcn3  26922  tgjustf  28751  tgjustr  28752  tgcgr4  28809  perpcom  29002  brbtwn2  29264  colinearalglem2  29266  eengtrkg  29345  isarchi2  33514  opprlidlabs  33776  elmrsubrn  36020  nmulprop  36690  nmulcom  36694  nadddilem2  36721  nadddilem4  36723  isbnd3b  38464  iscvlat2N  40126  ishlat3N  40156  gicabl  43854  lindslinindsimp2  49271  joindm3  49775  meetdm3  49777  fucofulem2  50117  thincpropd  50248  functhinclem1  50250  fulltermc  50317  postc  50375  islmd  50471  iscmd  50472