![]() |
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 3090 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∈ wcel 2107 ∀wral 3062 |
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 3063 |
This theorem is referenced by: ralbii 3094 ralanid 3096 poinxp 5754 soinxp 5755 seinxp 5757 dffun8 6573 funcnv3 6615 fncnv 6618 fnres 6674 fvreseq0 7035 isoini2 7331 smores 8347 tfr3ALT 8397 resixp 8923 ixpfi2 9346 marypha1lem 9424 ac5num 10027 acni2 10037 acndom 10042 dfac4 10113 brdom7disj 10522 brdom6disj 10523 fpwwe2lem7 10628 axgroth6 10819 rabssnn0fi 13947 lo1res 15499 isprm5 16640 prmreclem2 16846 tsrss 18538 gass 19159 efgval2 19585 efgsres 19599 acsfn1p 20403 isdomn2 20902 islinds2 21352 isclo 22573 ptclsg 23101 ufilcmp 23518 cfilres 24795 ovolgelb 24979 volsup2 25104 vitali 25112 itg1climres 25214 itg2seq 25242 itg2monolem1 25250 itg2mono 25253 itg2i1fseq 25255 itg2cn 25263 ellimc2 25376 rolle 25489 lhop1 25513 itgsubstlem 25547 tdeglem4 25559 tdeglem4OLD 25560 dvdsmulf1o 26678 dchrelbas2 26720 selbergsb 27058 axcontlem2 28203 dfconngr1 29421 hodsi 31006 ho01i 31059 ho02i 31060 lnopeqi 31239 nmcopexi 31258 nmcfnexi 31282 cnlnadjlem3 31300 cnlnadjlem5 31302 leop3 31356 pjssposi 31403 largei 31498 mdsl2i 31553 mdsl2bi 31554 elat2 31571 dmdbr5ati 31653 cdj3lem3b 31671 subfacp1lem3 34111 dfso3 34627 phpreu 36410 ptrecube 36426 mblfinlem1 36463 voliunnfl 36470 disjressuc2 37196 alephiso2 42242 ntrneiel2 42770 ismbl3 44637 ismbl4 44644 sge0lefimpt 45074 sbgoldbalt 46384 |
Copyright terms: Public domain | W3C validator |