Theorem 2ralbii 3109

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 3080	. 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)
3	2	ralbii 3080	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   ↔ wb 206  ∀wral 3049

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

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

This theorem is referenced by:  3ralbii  3111  ralnex3  3115  rmo4f  3691  2reu4lem  4474  cnvso  6244  fununi  6565  dff14a  7214  isocnv2  7275  f1opr  7412  sorpss  7671  xpord3inddlem  8094  tpossym  8198  dford2  9527  isffth2  17840  ispos2  18236  issubmgm  18625  issubm  18726  cntzrec  19263  oppgsubm  19289  opprirred  20356  opprsubrng  20490  rhmimasubrng  20497  cntzsubrng  20498  opprsubrg  20524  isdomn5  20641  isdomn3  20646  gsummatr01lem3  22599  gsummatr01  22601  isbasis2g  22890  ist0-3  23287  isfbas2  23777  isclmp  25051  addsproplem4  27942  addsproplem6  27944  addsprop  27946  negsproplem4  28000  negsproplem6  28002  negsprop  28004  mulsprop  28099  dfadj2  31909  adjval2  31915  cnlnadjeui  32101  adjbdln  32107  isarchi  33213  prmidl0  33480  ply1dg3rt0irred  33614  dff15  35189  iccllysconn  35393  dfso3  35863  elpotr  35922  dfon2  35933  idinxpss  38450  inxpssidinxp  38454  idinxpssinxp  38455  dfeldisj5  38919  isltrn2N  40319  hashnexinj  42321  fphpd  43000  fiinfi  43756  ntrk1k3eqk13  44233  ordelordALT  44720  dfac5prim  45173  disjinfi  45378  isthinc2  49607  isthinc3  49608