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 271 | . 2 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → 𝜓)) |
3 | 2 | ralbii2 3089 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∈ wcel 2104 ∀wral 3062 |
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 206 df-ral 3063 |
This theorem is referenced by: ralbii 3093 ralanid 3095 poinxp 5678 soinxp 5679 seinxp 5681 dffun8 6491 funcnv3 6533 fncnv 6536 fnres 6590 fvreseq0 6947 isoini2 7242 smores 8214 tfr3ALT 8264 resixp 8752 ixpfi2 9165 marypha1lem 9240 ac5num 9842 acni2 9852 acndom 9857 dfac4 9928 brdom7disj 10337 brdom6disj 10338 fpwwe2lem7 10443 axgroth6 10634 rabssnn0fi 13756 lo1res 15317 isprm5 16461 prmreclem2 16667 tsrss 18356 gass 18956 efgval2 19379 efgsres 19393 acsfn1p 20116 isdomn2 20619 islinds2 21069 isclo 22287 ptclsg 22815 ufilcmp 23232 cfilres 24509 ovolgelb 24693 volsup2 24818 vitali 24826 itg1climres 24928 itg2seq 24956 itg2monolem1 24964 itg2mono 24967 itg2i1fseq 24969 itg2cn 24977 ellimc2 25090 rolle 25203 lhop1 25227 itgsubstlem 25261 tdeglem4 25273 tdeglem4OLD 25274 dvdsmulf1o 26392 dchrelbas2 26434 selbergsb 26772 axcontlem2 27382 dfconngr1 28601 hodsi 30186 ho01i 30239 ho02i 30240 lnopeqi 30419 nmcopexi 30438 nmcfnexi 30462 cnlnadjlem3 30480 cnlnadjlem5 30482 leop3 30536 pjssposi 30583 largei 30678 mdsl2i 30733 mdsl2bi 30734 elat2 30751 dmdbr5ati 30833 cdj3lem3b 30851 subfacp1lem3 33193 dfso3 33713 phpreu 35809 ptrecube 35825 mblfinlem1 35862 voliunnfl 35869 disjressuc2 36602 alephiso2 41378 ntrneiel2 41909 ismbl3 43756 ismbl4 43763 sge0lefimpt 44191 sbgoldbalt 45477 |
Copyright terms: Public domain | W3C validator |