![]() |
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 3087 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∈ wcel 2106 ∀wral 3059 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 |
This theorem depends on definitions: df-bi 207 df-ral 3060 |
This theorem is referenced by: ralbii 3091 ralanid 3093 poinxp 5769 soinxp 5770 seinxp 5772 dffun8 6596 funcnv3 6638 fncnv 6641 fnres 6696 fvreseq0 7058 isoini2 7359 smores 8391 tfr3ALT 8441 resixp 8972 ixpfi2 9388 marypha1lem 9471 ac5num 10074 acni2 10084 acndom 10089 dfac4 10160 brdom7disj 10569 brdom6disj 10570 fpwwe2lem7 10675 axgroth6 10866 rabssnn0fi 14024 lo1res 15592 isprm5 16741 prmreclem2 16951 tsrss 18647 gass 19332 efgval2 19757 efgsres 19771 isdomn2 20728 isdomn2OLD 20729 acsfn1p 20817 islinds2 21851 isclo 23111 ptclsg 23639 ufilcmp 24056 cfilres 25344 ovolgelb 25529 volsup2 25654 vitali 25662 itg1climres 25764 itg2seq 25792 itg2monolem1 25800 itg2mono 25803 itg2i1fseq 25805 itg2cn 25813 ellimc2 25927 rolle 26043 lhop1 26068 itgsubstlem 26104 tdeglem4 26114 mpodvdsmulf1o 27252 dvdsmulf1o 27254 dchrelbas2 27296 selbergsb 27634 axcontlem2 28995 dfconngr1 30217 hodsi 31804 ho01i 31857 ho02i 31858 lnopeqi 32037 nmcopexi 32056 nmcfnexi 32080 cnlnadjlem3 32098 cnlnadjlem5 32100 leop3 32154 pjssposi 32201 largei 32296 mdsl2i 32351 mdsl2bi 32352 elat2 32369 dmdbr5ati 32451 cdj3lem3b 32469 subfacp1lem3 35167 dfso3 35700 phpreu 37591 ptrecube 37607 mblfinlem1 37644 voliunnfl 37651 disjressuc2 38370 fimgmcyc 42521 alephiso2 43548 ntrneiel2 44076 ismbl3 45942 ismbl4 45949 sge0lefimpt 46379 sbgoldbalt 47706 |
Copyright terms: Public domain | W3C validator |