![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rabbi | Structured version Visualization version GIF version |
Description: Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbii 3439. (Contributed by NM, 25-Nov-2013.) |
Ref | Expression |
---|---|
rabbi | ⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abbib 2805 | . 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜒)} ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒))) | |
2 | df-rab 3434 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} | |
3 | df-rab 3434 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜒} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜒)} | |
4 | 2, 3 | eqeq12i 2751 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒} ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜒)}) |
5 | df-ral 3063 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜓 ↔ 𝜒))) | |
6 | pm5.32 575 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → (𝜓 ↔ 𝜒)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒))) | |
7 | 6 | albii 1822 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜓 ↔ 𝜒)) ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒))) |
8 | 5, 7 | bitri 275 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒))) |
9 | 1, 4, 8 | 3bitr4ri 304 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∀wal 1540 = wceq 1542 ∈ wcel 2107 {cab 2710 ∀wral 3062 {crab 3433 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-ral 3063 df-rab 3434 |
This theorem is referenced by: rabbidaOLD 3471 kqfeq 23228 isr0 23241 rabeq12f 37025 eq0rabdioph 41514 eqrabdioph 41515 lerabdioph 41543 eluzrabdioph 41544 ltrabdioph 41546 nerabdioph 41547 dvdsrabdioph 41548 undisjrab 43065 ioodvbdlimc1lem2 44648 ioodvbdlimc2lem 44650 fourierdlem89 44911 fourierdlem91 44913 fourierdlem100 44922 fourierdlem108 44930 fourierdlem112 44934 ovn0 45282 issmfdmpt 45464 line2x 47440 line2y 47441 |
Copyright terms: Public domain | W3C validator |