Theorem 2ralbidva 3128

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 468	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒))
3	2	ralbidva 3111	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
4	3	ralbidva 3111	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  ∀wral 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3069

This theorem is referenced by:  disjxun  5072  reu3op  6195  opreu2reurex  6197  isocnv3  7203  isotr  7207  f1oweALT  7815  fnmpoovd  7927  pospropd  18045  tosso  18137  isipodrs  18255  mndpropd  18410  mhmpropd  18436  efgred  19354  cmnpropd  19396  ringpropd  19821  lmodprop2d  20185  lsspropd  20279  islmhm2  20300  lmhmpropd  20335  islindf4  21045  assapropd  21076  scmatmats  21660  cpmatel2  21862  1elcpmat  21864  m2cpminvid2  21904  decpmataa0  21917  pmatcollpw2lem  21926  connsub  22572  hausdiag  22796  ist0-4  22880  ismet2  23486  txmetcnp  23703  txmetcn  23704  metuel2  23721  metucn  23727  isngp3  23754  nlmvscn  23851  isclmp  24260  isncvsngp  24313  ipcn  24410  iscfil2  24430  caucfil  24447  cfilresi  24459  ulmdvlem3  25561  cxpcn3  25901  tgjustf  26834  tgjustr  26835  tgcgr4  26892  perpcom  27074  brbtwn2  27273  colinearalglem2  27275  eengtrkg  27354  isarchi2  31439  elmrsubrn  33482  isbnd3b  35943  iscvlat2N  37338  ishlat3N  37368  gicabl  40924  isdomn3  41029  mgmpropd  45329  mgmhmpropd  45339  lidlmmgm  45483  lindslinindsimp2  45804  joindm3  46263  meetdm3  46265  functhinclem1  46322  postc  46363