Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ralbii | GIF version |
Description: Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.) |
Ref | Expression |
---|---|
ralbii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
ralbii | ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralbii.1 | . . . 4 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | a1i 9 | . . 3 ⊢ (⊤ → (𝜑 ↔ 𝜓)) |
3 | 2 | ralbidv 2326 | . 2 ⊢ (⊤ → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)) |
4 | 3 | trud 1252 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 ⊤wtru 1244 ∀wral 2306 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-4 1400 ax-17 1419 |
This theorem depends on definitions: df-bi 110 df-tru 1246 df-nf 1350 df-ral 2311 |
This theorem is referenced by: 2ralbii 2332 ralinexa 2351 r3al 2366 r19.26-2 2442 r19.26-3 2443 ralbiim 2447 r19.28av 2449 cbvral2v 2541 cbvral3v 2543 sbralie 2546 ralcom4 2576 reu8 2737 2reuswapdc 2743 eqsnm 3526 uni0b 3605 uni0c 3606 ssint 3631 iuniin 3667 iuneq2 3673 iunss 3698 ssiinf 3706 iinab 3718 iindif2m 3724 iinin2m 3725 iinuniss 3737 sspwuni 3739 iinpw 3742 dftr3 3858 trint 3869 bnd2 3926 reusv3 4192 reg2exmidlema 4259 setindel 4263 ordsoexmid 4286 zfregfr 4298 tfi 4305 tfis2f 4307 ssrel2 4430 reliun 4458 xpiindim 4473 ralxpf 4482 dfse2 4698 rninxp 4764 dminxp 4765 cnviinm 4859 cnvpom 4860 cnvsom 4861 dffun9 4930 funco 4940 funcnv3 4961 fncnv 4965 funimaexglem 4982 fnres 5015 fnopabg 5022 mptfng 5024 fintm 5075 f1ompt 5320 idref 5396 dff13f 5409 foov 5647 oacl 6040 cauappcvgprlemladdrl 6755 axcaucvglemres 6973 cvg1nlemcau 9583 cvg1nlemres 9584 recvguniq 9593 resqrexlemglsq 9620 resqrexlemsqa 9622 resqrexlemex 9623 clim0 9806 |
Copyright terms: Public domain | W3C validator |