![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > opabbii | Structured version Visualization version GIF version |
Description: Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.) |
Ref | Expression |
---|---|
opabbii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
opabbii | ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2825 | . 2 ⊢ 𝑧 = 𝑧 | |
2 | opabbii.1 | . . . 4 ⊢ (𝜑 ↔ 𝜓) | |
3 | 2 | a1i 11 | . . 3 ⊢ (𝑧 = 𝑧 → (𝜑 ↔ 𝜓)) |
4 | 3 | opabbidv 4941 | . 2 ⊢ (𝑧 = 𝑧 → {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓}) |
5 | 1, 4 | ax-mp 5 | 1 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 = wceq 1656 {copab 4937 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-opab 4938 |
This theorem is referenced by: mptv 4976 2rbropap 5245 dfid4 5254 fconstmpt 5402 xpundi 5408 xpundir 5409 inxp 5491 csbcnv 5542 cnvco 5544 resopab 5687 opabresid 5702 cnvi 5782 cnvun 5783 cnvxp 5796 cnvcnv3 5827 coundi 5881 coundir 5882 mptun 6262 fvopab6 6564 fmptsng 6691 fmptsnd 6692 cbvoprab1 6992 cbvoprab12 6994 dmoprabss 7007 mpt2mptx 7016 resoprab 7021 elrnmpt2res 7039 ov6g 7063 1st2val 7461 2nd2val 7462 dfoprab3s 7490 dfoprab3 7491 dfoprab4 7492 opabn1stprc 7495 mptmpt2opabbrd 7516 fsplit 7551 mapsncnv 8177 xpcomco 8325 marypha2lem2 8617 oemapso 8863 leweon 9154 r0weon 9155 compsscnv 9515 fpwwe 9790 ltrelxr 10425 ltxrlt 10434 ltxr 12242 shftidt2 14205 prdsle 16482 prdsless 16483 prdsleval 16497 dfiso2 16791 joindm 17363 meetdm 17377 gaorb 18097 efgcpbllema 18527 frgpuplem 18545 ltbval 19839 ltbwe 19840 opsrle 19843 opsrtoslem1 19851 opsrtoslem2 19852 dvdsrzring 20198 pjfval2 20423 lmfval 21414 lmbr 21440 cnmptid 21842 lgsquadlem3 25527 perpln1 26029 outpasch 26071 ishpg 26075 axcontlem2 26271 wksfval 26914 wlkson 26960 pthsfval 27030 ispth 27032 dfadj2 29295 dmadjss 29297 cnvadj 29302 mpt2mptxf 30021 fneer 32881 bj-dfmpt2a 33589 bj-mpt2mptALT 33590 cnfinltrel 33781 opropabco 34056 cnvepres 34612 inxp2 34672 xrninxp 34693 xrninxp2 34694 rnxrnres 34700 rnxrncnvepres 34701 rnxrnidres 34702 dfcoss2 34714 dfcoss3 34715 1cossres 34727 dfcoels 34728 br1cosscnvxrn 34767 1cosscnvxrn 34768 coss0 34772 cossid 34773 dfssr2 34792 cmtfvalN 35280 cmtvalN 35281 cvrfval 35338 cvrval 35339 dicval2 37249 fgraphopab 38626 fgraphxp 38627 dfnelbr2 42169 opabbrfex0d 42183 opabbrfexd 42185 upwlksfval 42577 xpsnopab 42626 mpt2mptx2 42974 |
Copyright terms: Public domain | W3C validator |