Theorem 2ralbii 3137

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

Syntax hints:   ↔ wb 208  ∀wral 3076

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

This theorem depends on definitions:  df-bi 209  df-ral 3077

This theorem is referenced by:  3ralbii  3139  ralnex3  3143  rmo4f  3698  2reu4lem  4477  cnvso  6275  fununi  6596  dff14a  7254  isocnv2  7315  f1opr  7452  sorpss  7711  xpord3inddlem  8134  tpossym  8238  dford2  9575  isffth2  17951  ispos2  18347  issubmgm  18736  issubm  18837  cntzrec  19376  oppgsubm  19402  opprirred  20467  opprsubrng  20605  rhmimasubrng  20612  cntzsubrng  20613  opprsubrg  20639  isdomn5  20756  isdomn3  20761  gsummatr01lem3  22714  gsummatr01  22716  isbasis2g  23005  ist0-3  23402  isfbas2  23892  isclmp  25156  addsproplem4  28062  addsproplem6  28064  addsprop  28066  negsproplem4  28121  negsproplem6  28123  negsprop  28125  mulsprop  28220  dfadj2  32085  adjval2  32091  cnlnadjeui  32277  adjbdln  32283  isarchi  33359  prmidl0  33634  ply1dg3rt0irred  33777  dff15  35375  iccllysconn  35597  dfso3  36067  elpotr  36126  dfon2  36137  idinxpss  38814  inxpssidinxp  38818  idinxpssinxp  38819  dfdisjALTV5a  39299  dfeldisj5  39309  dfeldisj5a  39310  isltrn2N  40741  hashnexinj  42742  fphpd  43390  fiinfi  44146  ntrk1k3eqk13  44623  ordelordALT  45110  dfac5prim  45563  disjinfi  45767  isthinc2  50038  isthinc3  50039