| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > elrabf | Structured version Visualization version GIF version | ||
| Description: Membership in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.) |
| Ref | Expression |
|---|---|
| elrabf.1 | ⊢ Ⅎ𝑥𝐴 |
| elrabf.2 | ⊢ Ⅎ𝑥𝐵 |
| elrabf.3 | ⊢ Ⅎ𝑥𝜓 |
| elrabf.4 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| elrabf | ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elex 3501 | . 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} → 𝐴 ∈ V) | |
| 2 | elex 3501 | . . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | |
| 3 | 2 | adantr 480 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → 𝐴 ∈ V) |
| 4 | df-rab 3437 | . . . 4 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} | |
| 5 | 4 | eleq2i 2833 | . . 3 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}) |
| 6 | elrabf.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
| 7 | elrabf.2 | . . . . . 6 ⊢ Ⅎ𝑥𝐵 | |
| 8 | 6, 7 | nfel 2920 | . . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 |
| 9 | elrabf.3 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
| 10 | 8, 9 | nfan 1899 | . . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 ∧ 𝜓) |
| 11 | eleq1 2829 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
| 12 | elrabf.4 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
| 13 | 11, 12 | anbi12d 632 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))) |
| 14 | 6, 10, 13 | elabgf 3674 | . . 3 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))) |
| 15 | 5, 14 | bitrid 283 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))) |
| 16 | 1, 3, 15 | pm5.21nii 378 | 1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 Ⅎwnf 1783 ∈ wcel 2108 {cab 2714 Ⅎwnfc 2890 {crab 3436 Vcvv 3480 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-rab 3437 df-v 3482 |
| This theorem is referenced by: rabtru 3689 invdisjrab 5130 rabxfrd 5417 f1ossf1o 7148 onminsb 7814 nnawordex 8675 tskwe 9990 rabssnn0fi 14027 iundisj 25583 sltval2 27701 iundisjf 32602 iundisjfi 32798 bnj1388 35047 phpreu 37611 poimirlem26 37653 sticksstones1 42147 rfcnpre3 45038 rfcnpre4 45039 uzwo4 45058 disjinfi 45197 allbutfiinf 45431 fsumiunss 45590 fnlimfvre 45689 stoweidlem26 46041 stoweidlem27 46042 stoweidlem31 46046 stoweidlem34 46049 stoweidlem51 46066 stoweidlem52 46067 stoweidlem59 46074 fourierdlem20 46142 fourierdlem79 46200 pimdecfgtioc 46730 smfpimcclem 46822 prmdvdsfmtnof1lem1 47571 |
| Copyright terms: Public domain | W3C validator |