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

Syntax hints:   ↔ wb 206  ∀wral 3045

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 3046

This theorem is referenced by:  3ralbii  3111  ralnex3  3115  rmo4f  3709  2reu4lem  4488  cnvso  6264  fununi  6594  dff14a  7248  isocnv2  7309  f1opr  7448  sorpss  7707  xpord3inddlem  8136  tpossym  8240  dford2  9580  isffth2  17887  ispos2  18283  issubmgm  18636  issubm  18737  cntzrec  19275  oppgsubm  19301  opprirred  20338  opprsubrng  20475  rhmimasubrng  20482  cntzsubrng  20483  opprsubrg  20509  isdomn5  20626  isdomn3  20631  gsummatr01lem3  22551  gsummatr01  22553  isbasis2g  22842  ist0-3  23239  isfbas2  23729  isclmp  25004  addsproplem4  27886  addsproplem6  27888  addsprop  27890  negsproplem4  27944  negsproplem6  27946  negsprop  27948  mulsprop  28040  dfadj2  31821  adjval2  31827  cnlnadjeui  32013  adjbdln  32019  isarchi  33143  prmidl0  33428  ply1dg3rt0irred  33558  dff15  35081  iccllysconn  35244  dfso3  35714  elpotr  35776  dfon2  35787  idinxpss  38307  inxpssidinxp  38311  idinxpssinxp  38312  dfeldisj5  38720  isltrn2N  40121  hashnexinj  42123  fphpd  42811  fiinfi  43569  ntrk1k3eqk13  44046  ordelordALT  44534  dfac5prim  44987  disjinfi  45193  isthinc2  49413  isthinc3  49414