![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2ralbii | Structured version Visualization version GIF version |
Description: Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.) |
Ref | Expression |
---|---|
2ralbii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
2ralbii | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralbii.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | ralbii 3093 | . 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓) |
3 | 2 | ralbii 3093 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∀wral 3061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-ral 3062 |
This theorem is referenced by: ralnex3 3128 rmo4f 3697 2reu4lem 4487 cnvso 6244 fununi 6580 dff14a 7221 isocnv2 7280 f1opr 7417 sorpss 7669 xpord3inddlem 8090 tpossym 8193 dford2 9564 isffth2 17811 ispos2 18212 issubm 18622 cntzrec 19122 oppgsubm 19151 opprirred 20141 opprsubrg 20285 gsummatr01lem3 22029 gsummatr01 22031 isbasis2g 22321 ist0-3 22719 isfbas2 23209 isclmp 24483 addsproplem4 27313 addsproplem6 27315 addsprop 27317 negsproplem4 27358 negsproplem6 27360 negsprop 27362 dfadj2 30876 adjval2 30882 cnlnadjeui 31068 adjbdln 31074 isarchi 32074 prmidl0 32278 dff15 33752 iccllysconn 33908 dfso3 34355 elpotr 34419 dfon2 34430 3ralbii 36758 idinxpss 36823 inxpssidinxp 36827 idinxpssinxp 36828 dfeldisj5 37233 isltrn2N 38633 isdomn5 40673 fphpd 41186 isdomn3 41578 fiinfi 41937 ntrk1k3eqk13 42414 ordelordALT 42911 disjinfi 43504 issubmgm 46173 isthinc2 47132 isthinc3 47133 |
Copyright terms: Public domain | W3C validator |