Theorem 2ralbidva 3121

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3068

This theorem is referenced by:  disjxun  5068  reu3op  6184  opreu2reurex  6186  isocnv3  7183  isotr  7187  f1oweALT  7788  fnmpoovd  7898  pospropd  17960  tosso  18052  isipodrs  18170  mndpropd  18325  mhmpropd  18351  efgred  19269  cmnpropd  19311  ringpropd  19736  lmodprop2d  20100  lsspropd  20194  islmhm2  20215  lmhmpropd  20250  islindf4  20955  assapropd  20986  scmatmats  21568  cpmatel2  21770  1elcpmat  21772  m2cpminvid2  21812  decpmataa0  21825  pmatcollpw2lem  21834  connsub  22480  hausdiag  22704  ist0-4  22788  ismet2  23394  txmetcnp  23609  txmetcn  23610  metuel2  23627  metucn  23633  isngp3  23660  nlmvscn  23757  isclmp  24166  isncvsngp  24218  ipcn  24315  iscfil2  24335  caucfil  24352  cfilresi  24364  ulmdvlem3  25466  cxpcn3  25806  tgjustf  26738  tgjustr  26739  tgcgr4  26796  perpcom  26978  brbtwn2  27176  colinearalglem2  27178  eengtrkg  27257  isarchi2  31341  elmrsubrn  33382  isbnd3b  35870  iscvlat2N  37265  ishlat3N  37295  gicabl  40840  isdomn3  40945  mgmpropd  45217  mgmhmpropd  45227  lidlmmgm  45371  lindslinindsimp2  45692  joindm3  46151  meetdm3  46153  functhinclem1  46210  postc  46249