Theorem 2ralbidva 3217

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∈ wcel 2107  ∀wral 3062

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 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3063

This theorem is referenced by:  disjxun  5147  reu3op  6292  opreu2reurex  6294  isocnv3  7329  isotr  7333  f1oweALT  7959  fnmpoovd  8073  pospropd  18280  tosso  18372  isipodrs  18490  sgrppropd  18622  mndpropd  18650  mhmpropd  18678  efgred  19616  cmnpropd  19659  ringpropd  20102  lmodprop2d  20534  lsspropd  20628  islmhm2  20649  lmhmpropd  20684  islindf4  21393  assapropd  21426  scmatmats  22013  cpmatel2  22215  1elcpmat  22217  m2cpminvid2  22257  decpmataa0  22270  pmatcollpw2lem  22279  connsub  22925  hausdiag  23149  ist0-4  23233  ismet2  23839  txmetcnp  24056  txmetcn  24057  metuel2  24074  metucn  24080  isngp3  24107  nlmvscn  24204  isclmp  24613  isncvsngp  24666  ipcn  24763  iscfil2  24783  caucfil  24800  cfilresi  24812  ulmdvlem3  25914  cxpcn3  26256  tgjustf  27724  tgjustr  27725  tgcgr4  27782  perpcom  27964  brbtwn2  28163  colinearalglem2  28165  eengtrkg  28244  isarchi2  32331  opprlidlabs  32599  elmrsubrn  34511  isbnd3b  36653  iscvlat2N  38194  ishlat3N  38224  gicabl  41841  isdomn3  41946  mgmpropd  46545  mgmhmpropd  46555  rngpropd  46673  lindslinindsimp2  47144  joindm3  47602  meetdm3  47604  functhinclem1  47661  postc  47702