|   | 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 3088 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∈ wcel 2107 ∀wral 3060 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 | 
| This theorem depends on definitions: df-bi 207 df-ral 3061 | 
| This theorem is referenced by: ralbii 3092 ralanid 3094 poinxp 5765 soinxp 5766 seinxp 5768 dffun8 6593 funcnv3 6635 fncnv 6638 fnres 6694 fvreseq0 7057 isoini2 7360 smores 8393 tfr3ALT 8443 resixp 8974 ixpfi2 9391 marypha1lem 9474 ac5num 10077 acni2 10087 acndom 10092 dfac4 10163 brdom7disj 10572 brdom6disj 10573 fpwwe2lem7 10678 axgroth6 10869 rabssnn0fi 14028 lo1res 15596 isprm5 16745 prmreclem2 16956 tsrss 18635 gass 19320 efgval2 19743 efgsres 19757 isdomn2 20712 isdomn2OLD 20713 acsfn1p 20801 islinds2 21834 isclo 23096 ptclsg 23624 ufilcmp 24041 cfilres 25331 ovolgelb 25516 volsup2 25641 vitali 25649 itg1climres 25750 itg2seq 25778 itg2monolem1 25786 itg2mono 25789 itg2i1fseq 25791 itg2cn 25799 ellimc2 25913 rolle 26029 lhop1 26054 itgsubstlem 26090 tdeglem4 26100 mpodvdsmulf1o 27238 dvdsmulf1o 27240 dchrelbas2 27282 selbergsb 27620 axcontlem2 28981 dfconngr1 30208 hodsi 31795 ho01i 31848 ho02i 31849 lnopeqi 32028 nmcopexi 32047 nmcfnexi 32071 cnlnadjlem3 32089 cnlnadjlem5 32091 leop3 32145 pjssposi 32192 largei 32287 mdsl2i 32342 mdsl2bi 32343 elat2 32360 dmdbr5ati 32442 cdj3lem3b 32460 subfacp1lem3 35188 dfso3 35721 phpreu 37612 ptrecube 37628 mblfinlem1 37665 voliunnfl 37672 disjressuc2 38390 fimgmcyc 42549 alephiso2 43576 ntrneiel2 44104 wfac8prim 45024 ismbl3 46006 ismbl4 46013 sge0lefimpt 46443 sbgoldbalt 47773 | 
| Copyright terms: Public domain | W3C validator |