Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ralbiia | Structured version Visualization version GIF version |
Description: Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.) |
Ref | Expression |
---|---|
ralbiia.1 | ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
ralbiia | ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralbiia.1 | . . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) | |
2 | 1 | pm5.74i 259 | . 2 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → 𝜓)) |
3 | 2 | ralbii2 2961 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∈ wcel 1977 ∀wral 2896 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 |
This theorem depends on definitions: df-bi 196 df-ral 2901 |
This theorem is referenced by: poinxp 5105 soinxp 5106 seinxp 5108 dffun8 5831 funcnv3 5873 fncnv 5876 fnres 5921 fvreseq0 6225 isoini2 6489 smores 7336 tfr3ALT 7385 resixp 7829 ixpfi2 8147 marypha1lem 8222 ac5num 8742 acni2 8752 acndom 8757 dfac4 8828 brdom7disj 9234 brdom6disj 9235 fpwwe2lem8 9338 axgroth6 9529 rabssnn0fi 12647 lo1res 14138 isprm5 15257 prmreclem2 15459 tsrss 17046 gass 17557 efgval2 17960 efgsres 17974 isdomn2 19120 islinds2 19971 isclo 20701 ptclsg 21228 ufilcmp 21646 cfilres 22902 ovolgelb 23055 volsup2 23179 vitali 23188 itg1climres 23287 itg2seq 23315 itg2monolem1 23323 itg2mono 23326 itg2i1fseq 23328 itg2cn 23336 ellimc2 23447 rolle 23557 lhop1 23581 itgsubstlem 23615 tdeglem4 23624 dvdsmulf1o 24720 dchrelbas2 24762 selbergsb 25064 axcontlem2 25645 dfconngra1 26199 hodsi 28018 ho01i 28071 ho02i 28072 lnopeqi 28251 nmcopexi 28270 nmcfnexi 28294 cnlnadjlem3 28312 cnlnadjlem5 28314 leop3 28368 pjssposi 28415 largei 28510 mdsl2i 28565 mdsl2bi 28566 elat2 28583 dmdbr5ati 28665 cdj3lem3b 28683 subfacp1lem3 30418 dfso3 30856 phpreu 32563 ptrecube 32579 mblfinlem1 32616 voliunnfl 32623 acsfn1p 36788 ntrneiel2 37404 ismbl3 38879 ismbl4 38886 sge0lefimpt 39316 sgoldbalt 40203 dfconngr1 41355 |
Copyright terms: Public domain | W3C validator |