Theorem 2ralbii 3115

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

Syntax hints:   ↔ wb 206  ∀wral 3051

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 3052

This theorem is referenced by:  3ralbii  3117  ralnex3  3121  rmo4f  3718  2reu4lem  4497  cnvso  6277  fununi  6610  dff14a  7262  isocnv2  7323  f1opr  7461  sorpss  7720  xpord3inddlem  8151  tpossym  8255  dford2  9632  isffth2  17929  ispos2  18325  issubmgm  18678  issubm  18779  cntzrec  19317  oppgsubm  19343  opprirred  20380  opprsubrng  20517  rhmimasubrng  20524  cntzsubrng  20525  opprsubrg  20551  isdomn5  20668  isdomn3  20673  gsummatr01lem3  22593  gsummatr01  22595  isbasis2g  22884  ist0-3  23281  isfbas2  23771  isclmp  25046  addsproplem4  27922  addsproplem6  27924  addsprop  27926  negsproplem4  27980  negsproplem6  27982  negsprop  27984  mulsprop  28073  dfadj2  31812  adjval2  31818  cnlnadjeui  32004  adjbdln  32010  isarchi  33126  prmidl0  33411  ply1dg3rt0irred  33541  dff15  35061  iccllysconn  35218  dfso3  35683  elpotr  35745  dfon2  35756  idinxpss  38276  inxpssidinxp  38280  idinxpssinxp  38281  dfeldisj5  38685  isltrn2N  40085  hashnexinj  42087  fphpd  42786  fiinfi  43544  ntrk1k3eqk13  44021  ordelordALT  44510  dfac5prim  44963  disjinfi  45164  isthinc2  49254  isthinc3  49255