Theorem 2ralbidva 3137

Description: Formula-building rule for restricted universal quantifiers (deduction rule). (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 458	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒))
3	2	ralbidva 3134	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
4	3	ralbidva 3134	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   ∈ wcel 2145  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991

This theorem depends on definitions:  df-bi 197  df-an 383  df-ral 3066

This theorem is referenced by:  disjxun  4784  isocnv3  6725  isotr  6729  f1oweALT  7299  fnmpt2ovd  7402  fnmpt2ovdOLD  7403  tosso  17244  pospropd  17342  isipodrs  17369  mndpropd  17524  mhmpropd  17549  efgred  18368  cmnpropd  18409  ringpropd  18790  lmodprop2d  19135  lsspropd  19230  islmhm2  19251  lmhmpropd  19286  assapropd  19542  islindf4  20394  scmatmats  20535  cpmatel2  20738  1elcpmat  20740  m2cpminvid2  20780  decpmataa0  20793  pmatcollpw2lem  20802  connsub  21445  hausdiag  21669  ist0-4  21753  ismet2  22358  txmetcnp  22572  txmetcn  22573  metuel2  22590  metucn  22596  isngp3  22622  nlmvscn  22711  isclmp  23116  isncvsngp  23168  ipcn  23264  iscfil2  23283  caucfil  23300  cfilresi  23312  ulmdvlem3  24376  cxpcn3  24710  tgcgr4  25647  perpcom  25829  brbtwn2  26006  colinearalglem2  26008  eengtrkg  26086  isarchi2  30079  elmrsubrn  31755  isbnd3b  33916  iscvlat2N  35133  ishlat3N  35163  gicabl  38195  isdomn3  38308  mgmpropd  42303  mgmhmpropd  42313  lidlmmgm  42453  lindslinindsimp2  42780