Theorem 2ralbii 3128

Description: Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)

Hypothesis

Ref	Expression
2ralbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
2ralbii	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Proof of Theorem 2ralbii

Step	Hyp	Ref	Expression
1		2ralbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	ralbii 3093	. 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)
3	2	ralbii 3093	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   ↔ wb 206  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809

This theorem depends on definitions:  df-bi 207  df-ral 3062

This theorem is referenced by:  3ralbii  3130  ralnex3  3134  rmo4f  3741  2reu4lem  4522  cnvso  6308  fununi  6641  dff14a  7290  isocnv2  7351  f1opr  7489  sorpss  7748  xpord3inddlem  8179  tpossym  8283  dford2  9660  isffth2  17963  ispos2  18361  issubmgm  18715  issubm  18816  cntzrec  19354  oppgsubm  19381  opprirred  20422  opprsubrng  20559  rhmimasubrng  20566  cntzsubrng  20567  opprsubrg  20593  isdomn5  20710  isdomn3  20715  gsummatr01lem3  22663  gsummatr01  22665  isbasis2g  22955  ist0-3  23353  isfbas2  23843  isclmp  25130  addsproplem4  28005  addsproplem6  28007  addsprop  28009  negsproplem4  28063  negsproplem6  28065  negsprop  28067  mulsprop  28156  dfadj2  31904  adjval2  31910  cnlnadjeui  32096  adjbdln  32102  isarchi  33189  prmidl0  33478  ply1dg3rt0irred  33607  dff15  35098  iccllysconn  35255  dfso3  35720  elpotr  35782  dfon2  35793  idinxpss  38313  inxpssidinxp  38317  idinxpssinxp  38318  dfeldisj5  38722  isltrn2N  40122  hashnexinj  42129  fphpd  42827  fiinfi  43586  ntrk1k3eqk13  44063  ordelordALT  44557  dfac5prim  45007  disjinfi  45197  isthinc2  49070  isthinc3  49071