Theorem 2ralbidva 3216

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

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

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

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

This theorem is referenced by:  disjxun  5146  reu3op  6291  opreu2reurex  6293  isocnv3  7331  isotr  7335  f1oweALT  7961  fnmpoovd  8075  pospropd  18282  tosso  18374  isipodrs  18492  sgrppropd  18624  mndpropd  18652  mhmpropd  18680  efgred  19618  cmnpropd  19661  ringpropd  20104  lmodprop2d  20539  lsspropd  20633  islmhm2  20654  lmhmpropd  20689  islindf4  21399  assapropd  21432  scmatmats  22020  cpmatel2  22222  1elcpmat  22224  m2cpminvid2  22264  decpmataa0  22277  pmatcollpw2lem  22286  connsub  22932  hausdiag  23156  ist0-4  23240  ismet2  23846  txmetcnp  24063  txmetcn  24064  metuel2  24081  metucn  24087  isngp3  24114  nlmvscn  24211  isclmp  24620  isncvsngp  24673  ipcn  24770  iscfil2  24790  caucfil  24807  cfilresi  24819  ulmdvlem3  25921  cxpcn3  26263  tgjustf  27762  tgjustr  27763  tgcgr4  27820  perpcom  28002  brbtwn2  28201  colinearalglem2  28203  eengtrkg  28282  isarchi2  32372  opprlidlabs  32644  elmrsubrn  34580  isbnd3b  36739  iscvlat2N  38280  ishlat3N  38310  gicabl  41923  isdomn3  42028  mgmpropd  46624  mgmhmpropd  46634  rngpropd  46752  lindslinindsimp2  47222  joindm3  47680  meetdm3  47682  functhinclem1  47739  postc  47780